OAI/Computability/BinPacking/Arithmetic/NatExpressionBounds.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.BinaryRegisterProgram.addCommandInTime line 15
  2. def OAI.BinPackingGap.BinaryRegisterProgram.mulCommandInTime line 41
  3. def OAI.BinPackingGap.BinaryRegisterProgram.monusCommandInTime line 72
  4. def OAI.BinPackingGap.BinaryRegisterProgram.constantCommandInTime line 114
  5. def OAI.BinPackingGap.BinaryRegisterProgram.clearCommandInTime line 137
  6. def OAI.BinPackingGap.BinaryRegisterProgram.copyCommandInTime line 158
  7. def OAI.BinPackingGap.BinaryRegisterProgram.appendRuns line 201
  8. def OAI.BinPackingGap.BinaryRegisterProgram.commandInTime line 211
  9. def OAI.BinPackingGap.BinaryRegisterProgram.runInTime line 231
  10. def OAI.BinPackingGap.BinaryRegisterProgram.program line 250
  11. def OAI.BinPackingGap.BinaryRegisterProgram.programInTime line 254
  12. def OAI.BinPackingGap.BinaryRegisterProgram.BitBounded line 263
  13. def OAI.BinPackingGap.BinaryRegisterProgram.commandBound line 268
  14. theorem OAI.BinPackingGap.BinaryRegisterProgram.cost_le line 271
  15. theorem OAI.BinPackingGap.BinaryRegisterProgram.budget_le line 302
  16. def OAI.BinPackingGap.BinaryRegisterProgram.programInQuadraticTime line 317
  17. def OAI.BinPackingGap.BinaryRegisterProgram.runInQuadraticTime line 331
  18. def OAI.BinPackingGap.NatExpressionCompiler.compileInto line 355
  19. theorem OAI.BinPackingGap.NatExpressionCompiler.compileInto_correct line 373
  20. abbrev OAI.BinPackingGap.NatExpressionCompiler.Register line 418
  21. def OAI.BinPackingGap.NatExpressionCompiler.inputRegister line 420
  22. def OAI.BinPackingGap.NatExpressionCompiler.nodeRegister line 422
  23. theorem OAI.BinPackingGap.NatExpressionCompiler.registers_disjoint line 428
  24. def OAI.BinPackingGap.NatExpressionCompiler.initialValues line 432
  25. def OAI.BinPackingGap.NatExpressionCompiler.commands line 438
  26. theorem OAI.BinPackingGap.NatExpressionCompiler.commands_correct line 442
  27. theorem OAI.BinPackingGap.NatExpressionCompiler.commands_ready line 447
  28. theorem OAI.BinPackingGap.NatExpressionCompiler.commands_output line 452
  29. theorem OAI.BinPackingGap.NatExpressionCompiler.commands_preserve_input line 458
  30. def OAI.BinPackingGap.NatExpressionCompiler.compiledProgramInTime line 464
  31. theorem OAI.BinPackingGap.NatExpressionCompiler.compiled_output_tape line 479
  32. theorem OAI.BinPackingGap.NatExpressionCompiler.compiled_input_tape line 487
  33. def OAI.BinPackingGap.BinaryRegisterProgram.constantSize line 503
  34. def OAI.BinPackingGap.BinaryRegisterProgram.maxConstantSize line 507
  35. theorem OAI.BinPackingGap.BinaryRegisterProgram.constantSize_le_maxConstantSize line 512
  36. theorem OAI.BinPackingGap.BinaryRegisterProgram.result_size_le line 522
  37. theorem OAI.BinPackingGap.BinaryRegisterProgram.bitBounded_of_positive_width line 561
  38. def OAI.BinPackingGap.BinaryRegisterProgram.staticWidth line 589
  39. theorem OAI.BinPackingGap.BinaryRegisterProgram.bitBounded_from_input line 592
  40. def OAI.BinPackingGap.BinaryRegisterProgram.runtimePolynomial line 605
  41. theorem OAI.BinPackingGap.BinaryRegisterProgram.runtimePolynomial_eval line 612
  42. def OAI.BinPackingGap.BinaryRegisterProgram.programInPolynomialTime line 619
  43. def OAI.BinPackingGap.BinaryRegisterProgram.runInPolynomialTime line 632
  44. theorem OAI.BinPackingGap.NatExpressionCompiler.initialValues_size_le line 657
  45. def OAI.BinPackingGap.NatExpressionCompiler.timePolynomial line 665
  46. def OAI.BinPackingGap.NatExpressionCompiler.outputWidth line 668
  47. theorem OAI.BinPackingGap.NatExpressionCompiler.final_size_le line 671
  48. theorem OAI.BinPackingGap.NatExpressionCompiler.eval_size_le line 680
  49. def OAI.BinPackingGap.NatExpressionCompiler.compiledProgramInPolynomialTime line 691
  50. def OAI.BinPackingGap.NatExpressionCompiler.compiledRunInPolynomialTime line 708