OAI/Computability/BinPacking/Reductions/BinaryRenameLoop.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingCompleteness.BinaryRenameLoop.Token line 11
  2. def OAI.BinPackingCompleteness.BinaryRenameLoop.nextSlot line 13
  3. def OAI.BinPackingCompleteness.BinaryRenameLoop.clauseIncrement line 15
  4. def OAI.BinPackingCompleteness.BinaryRenameLoop.finalSlot line 17
  5. def OAI.BinPackingCompleteness.BinaryRenameLoop.completedClauses line 21
  6. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.finalSlot_three line 25
  7. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.completedClauses_three line 28
  8. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.finalSlot_triples line 32
  9. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.completedClauses_triples line 37
  10. def OAI.BinPackingCompleteness.BinaryRenameLoop.outputBody line 42
  11. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.outputBody_nil line 45
  12. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.outputBody_cons line 47
  13. def OAI.BinPackingCompleteness.BinaryRenameLoop.steps line 51
  14. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.payload_length_le_stream line 55
  15. def OAI.BinPackingCompleteness.BinaryRenameLoop.perLiteralBound line 70
  16. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.literal_steps_le line 73
  17. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.steps_le line 85
  18. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.steps_le_cubic line 98
  19. abbrev OAI.BinPackingCompleteness.BinaryRenameLoop.Alphabet line 116
  20. abbrev OAI.BinPackingCompleteness.BinaryRenameLoop.State line 117
  21. abbrev OAI.BinPackingCompleteness.BinaryRenameLoop.clean line 118
  22. inductive OAI.BinPackingCompleteness.BinaryRenameLoop.Label line 121
  23. def OAI.BinPackingCompleteness.BinaryRenameLoop.literalTapes line 127
  24. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.literalTapes_injective line 130
  25. def OAI.BinPackingCompleteness.BinaryRenameLoop.finish line 136
  26. def OAI.BinPackingCompleteness.BinaryRenameLoop.next line 142
  27. def OAI.BinPackingCompleteness.BinaryRenameLoop.instruction line 146
  28. def OAI.BinPackingCompleteness.BinaryRenameLoop.loopTapes line 162
  29. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.loopTapes_cursor line 167
  30. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.loopTapes_output line 173
  31. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.loopTapes_variables line 179
  32. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.loopTapes_clauses line 185
  33. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.update_cursor line 190
  34. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.update_output line 200
  35. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.update_variables line 210
  36. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.update_clauses line 220
  37. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.loopTapes_other line 226
  38. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.stepAux_finish line 232
  39. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.joinTrace line 237
  40. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.peekStep line 249
  41. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.emptyStep line 261
  42. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.tallyStep line 272
  43. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.bodyTrace line 287
  44. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.loopTrace line 359
  45. theorem OAI.BinPackingCompleteness.BinaryRenameLoop.triplesTrace line 403
  46. def OAI.BinPackingCompleteness.BinaryRenameLoop.triplesInTime line 420