OAI/Computability/BinPacking/Arithmetic/BinaryPowerMachine.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGap.BinaryMulMachine.Alphabet line 17
  2. abbrev OAI.BinPackingGap.BinaryMulMachine.State line 18
  3. def OAI.BinPackingGap.BinaryMulMachine.clean line 20
  4. inductive OAI.BinPackingGap.BinaryMulMachine.Label line 22
  5. abbrev OAI.BinPackingGap.BinaryMulMachine.Label.enumList line 28
  6. theorem OAI.BinPackingGap.BinaryMulMachine.Label.enumList_getElem?_ctorIdx_eq line 32
  7. theorem OAI.BinPackingGap.BinaryMulMachine.Label.enumList_nodup line 36
  8. instance OAI.BinPackingGap.BinaryMulMachine.(instance at line 38) line 38
  9. def OAI.BinPackingGap.BinaryMulMachine.statement line 42
  10. def OAI.BinPackingGap.BinaryMulMachine.program line 78
  11. def OAI.BinPackingGap.BinaryMulMachine.machine line 81
  12. def OAI.BinPackingGap.BinaryMulMachine.framedTapes line 92
  13. theorem OAI.BinPackingGap.BinaryMulMachine.framedTapes_slot line 96
  14. theorem OAI.BinPackingGap.BinaryMulMachine.framedTapes_other line 104
  15. theorem OAI.BinPackingGap.BinaryMulMachine.framedTapes_update line 109
  16. def OAI.BinPackingGap.BinaryMulMachine.tapes line 122
  17. def OAI.BinPackingGap.BinaryMulMachine.loopSteps line 128
  18. def OAI.BinPackingGap.BinaryMulMachine.steps line 136
  19. theorem OAI.BinPackingGap.BinaryMulMachine.tapes_slot line 139
  20. theorem OAI.BinPackingGap.BinaryMulMachine.tapes_update0 line 145
  21. theorem OAI.BinPackingGap.BinaryMulMachine.tapes_update1 line 156
  22. theorem OAI.BinPackingGap.BinaryMulMachine.tapes_update2 line 167
  23. theorem OAI.BinPackingGap.BinaryMulMachine.tapes_update3 line 178
  24. theorem OAI.BinPackingGap.BinaryMulMachine.tapes_update4 line 189
  25. theorem OAI.BinPackingGap.BinaryMulMachine.tapes_update5 line 200
  26. theorem OAI.BinPackingGap.BinaryMulMachine.tapes_update6 line 211
  27. theorem OAI.BinPackingGap.BinaryMulMachine.tapes_update7 line 222
  28. theorem OAI.BinPackingGap.BinaryMulMachine.tapes_update8 line 233
  29. theorem OAI.BinPackingGap.BinaryMulMachine.composeTrace line 244
  30. theorem OAI.BinPackingGap.BinaryMulMachine.copyInputsTrace line 257
  31. theorem OAI.BinPackingGap.BinaryMulMachine.guardEmptyTrace line 289
  32. theorem OAI.BinPackingGap.BinaryMulMachine.guardConsTrace line 299
  33. theorem OAI.BinPackingGap.BinaryMulMachine.shiftTrace line 309
  34. theorem OAI.BinPackingGap.BinaryMulMachine.addPhaseTrace line 319
  35. theorem OAI.BinPackingGap.BinaryMulMachine.cleanupTrace line 372
  36. theorem OAI.BinPackingGap.BinaryMulMachine.loopTrace line 417
  37. theorem OAI.BinPackingGap.BinaryMulMachine.multiplyTrace line 458
  38. theorem OAI.BinPackingGap.BinaryMulMachine.loopSteps_le line 470
  39. def OAI.BinPackingGap.BinaryMulMachine.timePolynomial line 503
  40. theorem OAI.BinPackingGap.BinaryMulMachine.steps_le_timePolynomial line 506
  41. def OAI.BinPackingGap.BinaryMulMachine.multiplyInTime line 517
  42. def OAI.BinPackingGap.BinaryMulMachine.multiplyInPolynomialTime line 531
  43. theorem OAI.BinPackingGap.BinaryMulMachine.multiplyNatTrace line 546
  44. theorem OAI.BinPackingGap.BinaryMulMachine.multiplyFrame line 558
  45. theorem OAI.BinPackingGap.BinaryMulMachine.initialTapes_eq line 565
  46. def OAI.BinPackingGap.BinaryMulMachine.multiplyNatInPolynomialTime line 582
  47. def OAI.BinPackingGap.BinaryMulMachine.programNatInPolynomialTime line 601
  48. inductive OAI.BinPackingGap.BinaryPowerMachine.Label line 623
  49. def OAI.BinPackingGap.BinaryPowerMachine.mulSlots line 628
  50. def OAI.BinPackingGap.BinaryPowerMachine.instruction line 635
  51. def OAI.BinPackingGap.BinaryPowerMachine.program line 653
  52. def OAI.BinPackingGap.BinaryPowerMachine.machine line 657
  53. theorem OAI.BinPackingGap.BinaryPowerMachine.machine_finiteAlphabet line 668
  54. def OAI.BinPackingGap.BinaryPowerMachine.Workspace line 673
  55. def OAI.BinPackingGap.BinaryPowerMachine.bodyBudget line 676
  56. def OAI.BinPackingGap.BinaryPowerMachine.loopBudget line 680
  57. def OAI.BinPackingGap.BinaryPowerMachine.appendRuns line 684
  58. def OAI.BinPackingGap.BinaryPowerMachine.bodyInTime line 706
  59. def OAI.BinPackingGap.BinaryPowerMachine.loopInTime line 812
  60. def OAI.BinPackingGap.BinaryPowerMachine.powerInTime line 861
  61. def OAI.BinPackingGap.BinaryPowerMachine.perIteration line 899
  62. theorem OAI.BinPackingGap.BinaryPowerMachine.loopBudget_le line 902
  63. def OAI.BinPackingGap.BinaryPowerMachine.timePolynomial line 923
  64. theorem OAI.BinPackingGap.BinaryPowerMachine.budget_le_timePolynomial line 926
  65. def OAI.BinPackingGap.BinaryPowerMachine.powerInPolynomialTime line 951