OAI/Computability/BinPacking/Reductions/BinaryTotalInputMachine.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingCompleteness.BinaryLanguage.rejectBinary line 10
  2. theorem OAI.BinPackingCompleteness.BinaryLanguage.rejectBinary_unsatisfiable line 14
  3. def OAI.BinPackingCompleteness.BinaryLanguage.rejectFormula line 23
  4. theorem OAI.BinPackingCompleteness.BinaryLanguage.reject_unsatisfiable line 25
  5. def OAI.BinPackingCompleteness.BinaryLanguage.language line 29
  6. def OAI.BinPackingCompleteness.BinaryLanguage.totalParsed line 32
  7. def OAI.BinPackingCompleteness.BinaryLanguage.totalRename line 35
  8. theorem OAI.BinPackingCompleteness.BinaryLanguage.totalParsed_satisfiable_iff line 38
  9. theorem OAI.BinPackingCompleteness.BinaryLanguage.totalRename_satisfiable_iff line 44
  10. theorem OAI.BinPackingCompleteness.BinaryLanguage.totalRename_encoded line 49
  11. theorem OAI.BinPackingCompleteness.BinaryLanguage.language_encoded line 53
  12. theorem OAI.BinPackingCompleteness.BinaryLanguage.reject_bits_length line 57
  13. theorem OAI.BinPackingCompleteness.BinaryLanguage.totalRename_output_length line 59
  14. inductive OAI.BinPackingCompleteness.BinaryTotalInputMachine.Label line 85
  15. abbrev OAI.BinPackingCompleteness.BinaryTotalInputMachine.Label.enumList line 92
  16. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.Label.enumList_getElem?_ctorIdx_eq line 94
  17. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.Label.enumList_nodup line 98
  18. instance OAI.BinPackingCompleteness.BinaryTotalInputMachine.(instance at line 100) line 100
  19. abbrev OAI.BinPackingCompleteness.BinaryTotalInputMachine.Alphabet line 104
  20. abbrev OAI.BinPackingCompleteness.BinaryTotalInputMachine.State line 105
  21. def OAI.BinPackingCompleteness.BinaryTotalInputMachine.rejectedWord line 107
  22. def OAI.BinPackingCompleteness.BinaryTotalInputMachine.instruction line 109
  23. abbrev OAI.BinPackingCompleteness.BinaryTotalInputMachine.machine line 123
  24. def OAI.BinPackingCompleteness.BinaryTotalInputMachine.tapes line 134
  25. def OAI.BinPackingCompleteness.BinaryTotalInputMachine.cfg line 139
  26. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.tapes_input line 143
  27. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.tapes_output line 146
  28. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.tapes_saved line 149
  29. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.update_input line 152
  30. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.update_output line 158
  31. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.update_saved line 164
  32. def OAI.BinPackingCompleteness.BinaryTotalInputMachine.afterScan line 170
  33. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.step_scan_empty line 172
  34. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.step_scan_cons line 179
  35. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.scanTrace line 187
  36. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.restoreTrace line 203
  37. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.drainTrace line 215
  38. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.step_rejectOutput line 226
  39. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.joinTrace line 236
  40. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.acceptedTrace line 240
  41. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.rejectedTrace line 251
  42. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.initList_eq line 266
  43. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.haltList_eq line 273
  44. def OAI.BinPackingCompleteness.BinaryTotalInputMachine.steps line 280
  45. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.steps_le line 283
  46. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.totalTrace line 287
  47. def OAI.BinPackingCompleteness.BinaryTotalInputMachine.outputsInTime line 309
  48. def OAI.BinPackingCompleteness.BinaryTotalInputMachine.computableInPolyTime line 317
  49. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.machine_finiteAlphabet line 331
  50. theorem OAI.BinPackingCompleteness.BinaryTotalInputMachine.computation_finiteAlphabet line 335