OAI/Computability/BinPacking/Reductions/BinaryLiteralMachine.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingCompleteness.BinaryLiteralMachine.Alphabet line 16
  2. abbrev OAI.BinPackingCompleteness.BinaryLiteralMachine.State line 17
  3. abbrev OAI.BinPackingCompleteness.BinaryLiteralMachine.clean line 18
  4. inductive OAI.BinPackingCompleteness.BinaryLiteralMachine.Label line 21
  5. def OAI.BinPackingCompleteness.BinaryLiteralMachine.searchTapes line 27
  6. theorem OAI.BinPackingCompleteness.BinaryLiteralMachine.searchTapes_injective line 36
  7. def OAI.BinPackingCompleteness.BinaryLiteralMachine.finish line 43
  8. def OAI.BinPackingCompleteness.BinaryLiteralMachine.readSign line 49
  9. def OAI.BinPackingCompleteness.BinaryLiteralMachine.emitSign line 57
  10. def OAI.BinPackingCompleteness.BinaryLiteralMachine.instruction line 63
  11. def OAI.BinPackingCompleteness.BinaryLiteralMachine.signWord line 83
  12. def OAI.BinPackingCompleteness.BinaryLiteralMachine.index line 85
  13. def OAI.BinPackingCompleteness.BinaryLiteralMachine.outputWord line 88
  14. def OAI.BinPackingCompleteness.BinaryLiteralMachine.steps line 91
  15. theorem OAI.BinPackingCompleteness.BinaryLiteralMachine.afterMatch_length_le line 97
  16. theorem OAI.BinPackingCompleteness.BinaryLiteralMachine.steps_le line 106
  17. theorem OAI.BinPackingCompleteness.BinaryLiteralMachine.stepAux_finish line 122
  18. theorem OAI.BinPackingCompleteness.BinaryLiteralMachine.joinTrace line 126
  19. theorem OAI.BinPackingCompleteness.BinaryLiteralMachine.literalTrace line 130
  20. def OAI.BinPackingCompleteness.BinaryLiteralMachine.literalInTime line 300