OAI/Computability/BinPacking/Reductions/BinaryHeaderMachine.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingCompleteness.BinaryHeaderMachine.Alphabet line 12
  2. abbrev OAI.BinPackingCompleteness.BinaryHeaderMachine.State line 13
  3. def OAI.BinPackingCompleteness.BinaryHeaderMachine.delimiter line 19
  4. def OAI.BinPackingCompleteness.BinaryHeaderMachine.tapes line 23
  5. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.tapes_variables line 28
  6. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.tapes_clauses line 35
  7. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.tapes_destination line 42
  8. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.tapes_other line 48
  9. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.update_variables line 54
  10. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.update_clauses line 71
  11. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.update_destination line 85
  12. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.clauseDelimiterStep line 104
  13. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.variableDelimiterStep line 116
  14. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.clauseCounterTrace line 128
  15. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.variableCounterTrace line 148
  16. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.joinTrace line 167
  17. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.headerTrace line 173
  18. def OAI.BinPackingCompleteness.BinaryHeaderMachine.headerInTime line 202
  19. abbrev OAI.BinPackingCompleteness.BinaryHeaderMachine.ConcreteTape line 217
  20. abbrev OAI.BinPackingCompleteness.BinaryHeaderMachine.ConcreteLabel line 218
  21. def OAI.BinPackingCompleteness.BinaryHeaderMachine.concreteProgram line 220
  22. abbrev OAI.BinPackingCompleteness.BinaryHeaderMachine.machine line 227
  23. def OAI.BinPackingCompleteness.BinaryHeaderMachine.start line 238
  24. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.haltList_eq line 242
  25. def OAI.BinPackingCompleteness.BinaryHeaderMachine.machineInTime line 250
  26. theorem OAI.BinPackingCompleteness.BinaryHeaderMachine.machine_finiteAlphabet line 260