OAI/Computability/BinPacking/Computation/MachinePortReindex.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.Alphabet line 12
  2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.State line 13
  3. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.residue line 15
  4. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.nextResidue line 18
  5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.nextResidue_residue line 21
  6. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.scanLoop line 27
  7. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.emitter line 40
  8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.scanPushBound line 47
  9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.emitterPushBound line 53
  10. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.tapes line 60
  11. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes line 64
  12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_source line 69
  13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_quotient line 77
  14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_remainder line 84
  15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.unaryTapes_other line 91
  16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.update_source line 99
  17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.update_quotient line 117
  18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.update_remainder line 131
  19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.scanAux_true line 137
  20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.scanAux_false line 153
  21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.scanStep_succ line 166
  22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.scanStep_zero line 193
  23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.emitterStep line 216
  24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.trace_fromCount line 240
  25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.divModTrace line 277
  26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.divModFromTapes line 298
  27. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.divModInTime line 325
  28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.scanTrace_fromCount line 349
  29. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinish line 382
  30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishPushBound line 390
  31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishStep line 398
  32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.divModTraceWithFinish line 424
  33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedDivMod.divModFromTapesWithFinish line 452
  34. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.Alphabet line 491
  35. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.State line 492
  36. def OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.clean line 494
  37. inductive OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.Label line 497
  38. def OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.exitAt line 503
  39. def OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.emit line 508
  40. def OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.instruction line 513
  41. def OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.steps line 534
  42. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.steps_le line 536
  43. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.steps_le_encodedLength line 541
  44. def OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.value line 547
  45. def OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.frame line 549
  46. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.joinTrace line 553
  47. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.reindexTrace line 557
  48. def OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.reindexInTime line 713
  49. def OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.machine line 732
  50. def OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.machineInTime line 743
  51. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePortReindex.lazy_value line 757