OAI/Computability/BinPacking/Arithmetic/NatExpressionBranch.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.BinaryAddPreserving.Label line 17
  2. abbrev OAI.BinPackingGap.BinaryAddPreserving.Label.enumList line 21
  3. theorem OAI.BinPackingGap.BinaryAddPreserving.Label.enumList_getElem?_ctorIdx_eq line 24
  4. theorem OAI.BinPackingGap.BinaryAddPreserving.Label.enumList_nodup line 28
  5. instance OAI.BinPackingGap.BinaryAddPreserving.(instance at line 30) line 30
  6. def OAI.BinPackingGap.BinaryAddPreserving.instruction line 34
  7. def OAI.BinPackingGap.BinaryAddPreserving.resultTapes line 48
  8. theorem OAI.BinPackingGap.BinaryAddPreserving.resultTapes_output line 51
  9. theorem OAI.BinPackingGap.BinaryAddPreserving.resultTapes_other line 54
  10. def OAI.BinPackingGap.BinaryAddPreserving.steps line 58
  11. theorem OAI.BinPackingGap.BinaryAddPreserving.steps_le line 61
  12. theorem OAI.BinPackingGap.BinaryAddPreserving.joinTrace line 66
  13. theorem OAI.BinPackingGap.BinaryAddPreserving.addTrace line 70
  14. def OAI.BinPackingGap.BinaryAddPreserving.addInTime line 172
  15. def OAI.BinPackingGap.BinaryAddPreserving.addInLinearTime line 189
  16. def OAI.BinPackingGap.BinaryAddPreserving.machine line 206
  17. theorem OAI.BinPackingGap.BinaryAddPreserving.machine_finiteAlphabet line 217
  18. def OAI.BinPackingGap.BinaryMonusMachine.subtractLoop line 233
  19. theorem OAI.BinPackingGap.BinaryMonusMachine.step_done line 255
  20. theorem OAI.BinPackingGap.BinaryMonusMachine.step_more line 265
  21. theorem OAI.BinPackingGap.BinaryMonusMachine.subtractTrace line 287
  22. def OAI.BinPackingGap.BinaryMonusMachine.subtractInTime line 328
  23. def OAI.BinPackingGap.BinaryMonusMachine.trimSteps line 343
  24. theorem OAI.BinPackingGap.BinaryMonusMachine.trimSteps_le line 347
  25. def OAI.BinPackingGap.BinaryMonusMachine.trimLoop line 354
  26. theorem OAI.BinPackingGap.BinaryMonusMachine.trimTrace line 365
  27. def OAI.BinPackingGap.BinaryMonusMachine.trimInTime line 392
  28. inductive OAI.BinPackingGap.BinaryMonusPreserving.Label line 421
  29. abbrev OAI.BinPackingGap.BinaryMonusPreserving.Label.enumList line 425
  30. theorem OAI.BinPackingGap.BinaryMonusPreserving.Label.enumList_getElem?_ctorIdx_eq line 428
  31. theorem OAI.BinPackingGap.BinaryMonusPreserving.Label.enumList_nodup line 432
  32. instance OAI.BinPackingGap.BinaryMonusPreserving.(instance at line 434) line 434
  33. def OAI.BinPackingGap.BinaryMonusPreserving.instruction line 438
  34. def OAI.BinPackingGap.BinaryMonusPreserving.resultTapes line 454
  35. theorem OAI.BinPackingGap.BinaryMonusPreserving.resultTapes_other line 457
  36. def OAI.BinPackingGap.BinaryMonusPreserving.budget line 461
  37. theorem OAI.BinPackingGap.BinaryMonusPreserving.budget_le line 464
  38. def OAI.BinPackingGap.BinaryMonusPreserving.appendRuns line 468
  39. def OAI.BinPackingGap.BinaryMonusPreserving.enlarge line 482
  40. def OAI.BinPackingGap.BinaryMonusPreserving.monusInTime line 489
  41. def OAI.BinPackingGap.BinaryMonusPreserving.monusInLinearTime line 637
  42. def OAI.BinPackingGap.BinaryMonusPreserving.machine line 650
  43. theorem OAI.BinPackingGap.BinaryMonusPreserving.machine_finiteAlphabet line 661
  44. inductive OAI.BinPackingGap.BinaryRegisterProgram.Command line 674
  45. def OAI.BinPackingGap.BinaryRegisterProgram.destination line 684
  46. def OAI.BinPackingGap.BinaryRegisterProgram.value line 688
  47. def OAI.BinPackingGap.BinaryRegisterProgram.result line 697
  48. def OAI.BinPackingGap.BinaryRegisterProgram.commandReady line 700
  49. def OAI.BinPackingGap.BinaryRegisterProgram.Ready line 705
  50. def OAI.BinPackingGap.BinaryRegisterProgram.resultOf line 710
  51. theorem OAI.BinPackingGap.BinaryRegisterProgram.result_destination line 713
  52. theorem OAI.BinPackingGap.BinaryRegisterProgram.result_other line 717
  53. theorem OAI.BinPackingGap.BinaryRegisterProgram.resultOf_nil line 721
  54. theorem OAI.BinPackingGap.BinaryRegisterProgram.resultOf_cons line 723
  55. theorem OAI.BinPackingGap.BinaryRegisterProgram.resultOf_append line 727
  56. theorem OAI.BinPackingGap.BinaryRegisterProgram.Ready_append line 734
  57. def OAI.BinPackingGap.BinaryRegisterProgram.cost line 742
  58. def OAI.BinPackingGap.BinaryRegisterProgram.budget line 753
  59. def OAI.BinPackingGap.BinaryRegisterProgram.LocalLabel line 756
  60. instance OAI.BinPackingGap.BinaryRegisterProgram.(instance at line 763) line 763
  61. instance OAI.BinPackingGap.BinaryRegisterProgram.(instance at line 766) line 766
  62. def OAI.BinPackingGap.BinaryRegisterProgram.main line 769
  63. def OAI.BinPackingGap.BinaryRegisterProgram.localInstruction line 776
  64. abbrev OAI.BinPackingGap.BinaryRegisterProgram.Label line 795
  65. def OAI.BinPackingGap.BinaryRegisterProgram.entry line 797
  66. def OAI.BinPackingGap.BinaryRegisterProgram.instruction line 800
  67. inductive OAI.BinPackingGap.NatExpressionCompiler.BinaryOp line 811
  68. instance OAI.BinPackingGap.NatExpressionCompiler.(instance at line 817) line 817
  69. def OAI.BinPackingGap.NatExpressionCompiler.applyOp line 821
  70. def OAI.BinPackingGap.NatExpressionCompiler.command line 828
  71. theorem OAI.BinPackingGap.NatExpressionCompiler.destination_command line 833
  72. theorem OAI.BinPackingGap.NatExpressionCompiler.value_command line 837
  73. theorem OAI.BinPackingGap.NatExpressionCompiler.commandReady_command line 843
  74. def OAI.BinPackingGap.NatExpressionCompiler.leftReg line 848
  75. def OAI.BinPackingGap.NatExpressionCompiler.rightReg line 854
  76. theorem OAI.BinPackingGap.NatExpressionCompiler.leftReg_apply line 860
  77. theorem OAI.BinPackingGap.NatExpressionCompiler.rightReg_apply line 863
  78. theorem OAI.BinPackingGap.NatExpressionCompiler.leftReg_ne_rightReg line 866
  79. theorem OAI.BinPackingGap.NatExpressionCompiler.root_ne_leftReg line 873
  80. theorem OAI.BinPackingGap.NatExpressionCompiler.root_ne_rightReg line 880
  81. def OAI.BinPackingGap.NatExpressionCompiler.branchOperands line 887
  82. theorem OAI.BinPackingGap.NatExpressionCompiler.branchOperands_destination line 896
  83. theorem OAI.BinPackingGap.NatExpressionCompiler.branchOperands_left line 900
  84. theorem OAI.BinPackingGap.NatExpressionCompiler.branchOperands_right line 904
  85. theorem OAI.BinPackingGap.NatExpressionCompiler.result_command_destination line 910
  86. def OAI.BinPackingGap.NatExpressionCompiler.Correct line 917
  87. theorem OAI.BinPackingGap.NatExpressionCompiler.branchCorrect line 924