OAI/Computability/BinPacking/Reductions/BinaryInputReduction.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingCompleteness.BinaryRenameMachine.Tape line 15
  2. abbrev OAI.BinPackingCompleteness.BinaryRenameMachine.Alphabet line 16
  3. abbrev OAI.BinPackingCompleteness.BinaryRenameMachine.State line 17
  4. inductive OAI.BinPackingCompleteness.BinaryRenameMachine.Label line 19
  5. def OAI.BinPackingCompleteness.BinaryRenameMachine.loopTapes line 26
  6. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.loopTapes_injective line 28
  7. def OAI.BinPackingCompleteness.BinaryRenameMachine.program line 33
  8. abbrev OAI.BinPackingCompleteness.BinaryRenameMachine.machine line 46
  9. def OAI.BinPackingCompleteness.BinaryRenameMachine.tapes line 57
  10. def OAI.BinPackingCompleteness.BinaryRenameMachine.cfg line 67
  11. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.initList_eq line 72
  12. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.haltList_eq line 79
  13. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.copyTrace line 86
  14. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.restoreTrace line 103
  15. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.headerTrace line 124
  16. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.cleanupTrace line 148
  17. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.outputBody_eq line 166
  18. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.loopTrace line 181
  19. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.joinTrace line 224
  20. def OAI.BinPackingCompleteness.BinaryRenameMachine.steps line 228
  21. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.renameTrace line 235
  22. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.clause_count_le_stream line 254
  23. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.body_length_le line 259
  24. def OAI.BinPackingCompleteness.BinaryRenameMachine.timePolynomial line 270
  25. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.steps_le line 274
  26. def OAI.BinPackingCompleteness.BinaryRenameMachine.outputsInTime line 294
  27. def OAI.BinPackingCompleteness.BinaryRenameMachine.tokenComputation line 302
  28. def OAI.BinPackingCompleteness.BinaryRenameMachine.preprocessing line 315
  29. def OAI.BinPackingCompleteness.BinaryRenameMachine.computableInPolyTime line 325
  30. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.machine_finiteAlphabet line 330
  31. theorem OAI.BinPackingCompleteness.BinaryRenameMachine.computation_finiteAlphabet line 334
  32. def OAI.BinPackingCompleteness.BinaryInputReduction.computation line 344
  33. theorem OAI.BinPackingCompleteness.BinaryInputReduction.computation_finiteAlphabet line 351
  34. def OAI.BinPackingCompleteness.BinaryInputReduction.reduction line 357
  35. theorem OAI.BinPackingCompleteness.BinaryInputReduction.reduction_finiteAlphabet line 362