OAI/Computability/BinPacking/Reductions/BinaryPairMachine.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingCompleteness.BinaryPairMachine.Tape line 12
  2. abbrev OAI.BinPackingCompleteness.BinaryPairMachine.Label line 13
  3. abbrev OAI.BinPackingCompleteness.BinaryPairMachine.State line 14
  4. abbrev OAI.BinPackingCompleteness.BinaryPairMachine.Alphabet line 15
  5. def OAI.BinPackingCompleteness.BinaryPairMachine.stop line 17
  6. def OAI.BinPackingCompleteness.BinaryPairMachine.count line 20
  7. def OAI.BinPackingCompleteness.BinaryPairMachine.copy line 28
  8. def OAI.BinPackingCompleteness.BinaryPairMachine.program line 37
  9. abbrev OAI.BinPackingCompleteness.BinaryPairMachine.machine line 43
  10. def OAI.BinPackingCompleteness.BinaryPairMachine.tapes line 54
  11. def OAI.BinPackingCompleteness.BinaryPairMachine.cfg line 57
  12. theorem OAI.BinPackingCompleteness.BinaryPairMachine.tapes_zero line 61
  13. theorem OAI.BinPackingCompleteness.BinaryPairMachine.tapes_one line 64
  14. theorem OAI.BinPackingCompleteness.BinaryPairMachine.tapes_two line 67
  15. theorem OAI.BinPackingCompleteness.BinaryPairMachine.update_zero line 70
  16. theorem OAI.BinPackingCompleteness.BinaryPairMachine.update_one line 76
  17. theorem OAI.BinPackingCompleteness.BinaryPairMachine.update_two line 82
  18. theorem OAI.BinPackingCompleteness.BinaryPairMachine.countStep_true line 88
  19. theorem OAI.BinPackingCompleteness.BinaryPairMachine.countStep_false line 95
  20. theorem OAI.BinPackingCompleteness.BinaryPairMachine.countTrace line 102
  21. theorem OAI.BinPackingCompleteness.BinaryPairMachine.copyStep_empty line 121
  22. theorem OAI.BinPackingCompleteness.BinaryPairMachine.copyStep_cons line 128
  23. theorem OAI.BinPackingCompleteness.BinaryPairMachine.copyTrace line 136
  24. theorem OAI.BinPackingCompleteness.BinaryPairMachine.restoreTrace line 151
  25. theorem OAI.BinPackingCompleteness.BinaryPairMachine.initList_eq line 164
  26. theorem OAI.BinPackingCompleteness.BinaryPairMachine.joinTrace line 171
  27. theorem OAI.BinPackingCompleteness.BinaryPairMachine.pairTrace line 175
  28. def OAI.BinPackingCompleteness.BinaryPairMachine.pairInTime line 190
  29. theorem OAI.BinPackingCompleteness.BinaryPairMachine.haltStep line 198
  30. def OAI.BinPackingCompleteness.BinaryPairMachine.pairHaltInTime line 204
  31. theorem OAI.BinPackingCompleteness.BinaryPairMachine.pairSteps_le_pairedLength line 216
  32. theorem OAI.BinPackingCompleteness.BinaryPairMachine.machine_finiteAlphabet line 222