OAI/Computability/BinPacking/PCP/NormalizationMachine.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingCompleteness.NormalizationMachine.Tape line 11
  2. abbrev OAI.BinPackingCompleteness.NormalizationMachine.Alphabet line 12
  3. abbrev OAI.BinPackingCompleteness.NormalizationMachine.State line 13
  4. inductive OAI.BinPackingCompleteness.NormalizationMachine.Label line 15
  5. def OAI.BinPackingCompleteness.NormalizationMachine.loopTapes line 21
  6. theorem OAI.BinPackingCompleteness.NormalizationMachine.loopTapes_injective line 23
  7. def OAI.BinPackingCompleteness.NormalizationMachine.program line 28
  8. abbrev OAI.BinPackingCompleteness.NormalizationMachine.machine line 40
  9. def OAI.BinPackingCompleteness.NormalizationMachine.tapes line 51
  10. def OAI.BinPackingCompleteness.NormalizationMachine.cfg line 55
  11. theorem OAI.BinPackingCompleteness.NormalizationMachine.initList_eq line 59
  12. theorem OAI.BinPackingCompleteness.NormalizationMachine.haltList_eq line 66
  13. theorem OAI.BinPackingCompleteness.NormalizationMachine.joinTrace line 73
  14. theorem OAI.BinPackingCompleteness.NormalizationMachine.readVariablesTrace line 77
  15. theorem OAI.BinPackingCompleteness.NormalizationMachine.readCountTrace line 92
  16. theorem OAI.BinPackingCompleteness.NormalizationMachine.headersTrace line 108
  17. theorem OAI.BinPackingCompleteness.NormalizationMachine.restoreTrace line 118
  18. theorem OAI.BinPackingCompleteness.NormalizationMachine.headerOutputTrace line 137
  19. theorem OAI.BinPackingCompleteness.NormalizationMachine.loopTrace line 158
  20. theorem OAI.BinPackingCompleteness.NormalizationMachine.formulaBits_eq line 189
  21. def OAI.BinPackingCompleteness.NormalizationMachine.steps line 195
  22. theorem OAI.BinPackingCompleteness.NormalizationMachine.normalizationTrace line 201
  23. theorem OAI.BinPackingCompleteness.NormalizationMachine.header_counts_le line 217
  24. def OAI.BinPackingCompleteness.NormalizationMachine.timePolynomial line 224
  25. theorem OAI.BinPackingCompleteness.NormalizationMachine.steps_le line 227
  26. def OAI.BinPackingCompleteness.NormalizationMachine.outputsInTime line 251
  27. def OAI.BinPackingCompleteness.NormalizationMachine.computableInPolyTime line 259
  28. theorem OAI.BinPackingCompleteness.NormalizationMachine.machine_finiteAlphabet line 271
  29. theorem OAI.BinPackingCompleteness.NormalizationMachine.computation_finiteAlphabet line 275