OAI/Computability/BinPacking/Arithmetic/BinaryTallyMachine.lean

GitHub source file

150 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGap.BinaryArithmetic.bitValue line 12
  2. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_nil line 14
  3. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_cons line 16
  4. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_bits line 19
  5. def OAI.BinPackingGap.BinaryArithmetic.Canonical line 22
  6. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_eq_zero_iff line 26
  7. theorem OAI.BinPackingGap.BinaryArithmetic.canonical_bits line 44
  8. theorem OAI.BinPackingGap.BinaryArithmetic.bits_bitValue line 55
  9. theorem OAI.BinPackingGap.BinaryArithmetic.canonical_length line 66
  10. def OAI.BinPackingGap.BinaryArithmetic.sumBit line 71
  11. def OAI.BinPackingGap.BinaryArithmetic.carryBit line 73
  12. def OAI.BinPackingGap.BinaryArithmetic.addCarry line 75
  13. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_addCarry line 88
  14. theorem OAI.BinPackingGap.BinaryArithmetic.addCarry_eq_nil line 109
  15. theorem OAI.BinPackingGap.BinaryArithmetic.canonical_addCarry line 113
  16. theorem OAI.BinPackingGap.BinaryArithmetic.addCarry_bits line 149
  17. theorem OAI.BinPackingGap.BinaryArithmetic.addCarry_length line 154
  18. theorem OAI.BinPackingGap.BinaryArithmetic.size_add_le line 175
  19. theorem OAI.BinPackingGap.BinaryArithmetic.size_mul_le line 180
  20. theorem OAI.BinPackingGap.BinaryArithmetic.size_pow_le line 185
  21. def OAI.BinPackingGap.BinaryArithmetic.shift line 197
  22. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_shift line 200
  23. theorem OAI.BinPackingGap.BinaryArithmetic.canonical_shift line 204
  24. theorem OAI.BinPackingGap.BinaryArithmetic.shift_length_le line 210
  25. theorem OAI.BinPackingGap.BinaryArithmetic.shift_bits line 213
  26. def OAI.BinPackingGap.BinaryArithmetic.mulAcc line 217
  27. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_mulAcc line 222
  28. theorem OAI.BinPackingGap.BinaryArithmetic.canonical_mulAcc line 229
  29. theorem OAI.BinPackingGap.BinaryArithmetic.mulAcc_bits line 242
  30. theorem OAI.BinPackingGap.BinaryArithmetic.mulAcc_bits_length line 247
  31. def OAI.BinPackingGap.BinaryArithmetic.powTally line 251
  32. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_powTally line 255
  33. theorem OAI.BinPackingGap.BinaryArithmetic.canonical_powTally line 262
  34. theorem OAI.BinPackingGap.BinaryArithmetic.powTally_bits line 269
  35. theorem OAI.BinPackingGap.BinaryArithmetic.powTally_bits_length line 274
  36. def OAI.BinPackingGap.BinaryArithmetic.powAcc line 278
  37. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_powAcc line 282
  38. theorem OAI.BinPackingGap.BinaryArithmetic.canonical_powAcc line 290
  39. theorem OAI.BinPackingGap.BinaryArithmetic.powAcc_bits line 298
  40. theorem OAI.BinPackingGap.BinaryArithmetic.powAcc_bits_length line 303
  41. theorem OAI.BinPackingGap.BinaryArithmetic.powAcc_bits_length_take line 310
  42. def OAI.BinPackingGap.BinaryArithmetic.consBit line 317
  43. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_consBit line 321
  44. theorem OAI.BinPackingGap.BinaryArithmetic.canonical_consBit line 325
  45. theorem OAI.BinPackingGap.BinaryArithmetic.consBit_length_le line 331
  46. def OAI.BinPackingGap.BinaryArithmetic.trim line 335
  47. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_trim line 339
  48. theorem OAI.BinPackingGap.BinaryArithmetic.canonical_trim line 344
  49. theorem OAI.BinPackingGap.BinaryArithmetic.trim_eq_bits line 349
  50. theorem OAI.BinPackingGap.BinaryArithmetic.trim_length_le line 353
  51. def OAI.BinPackingGap.BinaryArithmetic.trimHigh line 361
  52. theorem OAI.BinPackingGap.BinaryArithmetic.trimHigh_append line 366
  53. theorem OAI.BinPackingGap.BinaryArithmetic.trimHigh_reverse line 379
  54. theorem OAI.BinPackingGap.BinaryArithmetic.trimHigh_length_le line 389
  55. def OAI.BinPackingGap.BinaryArithmetic.diffBit line 396
  56. def OAI.BinPackingGap.BinaryArithmetic.borrowBit line 398
  57. def OAI.BinPackingGap.BinaryArithmetic.subBorrow line 400
  58. def OAI.BinPackingGap.BinaryArithmetic.rawSubtract line 413
  59. theorem OAI.BinPackingGap.BinaryArithmetic.subBorrow_eq_rawSubtract line 429
  60. theorem OAI.BinPackingGap.BinaryArithmetic.rawSubtract_length line 454
  61. def OAI.BinPackingGap.BinaryArithmetic.BorrowSpec line 475
  62. theorem OAI.BinPackingGap.BinaryArithmetic.borrowSpec_step line 479
  63. theorem OAI.BinPackingGap.BinaryArithmetic.subBorrow_spec line 496
  64. theorem OAI.BinPackingGap.BinaryArithmetic.subBorrow_none_iff line 520
  65. theorem OAI.BinPackingGap.BinaryArithmetic.subBorrow_some_value line 531
  66. def OAI.BinPackingGap.BinaryArithmetic.monus line 536
  67. theorem OAI.BinPackingGap.BinaryArithmetic.bitValue_monus line 538
  68. theorem OAI.BinPackingGap.BinaryArithmetic.canonical_monus line 552
  69. theorem OAI.BinPackingGap.BinaryArithmetic.monus_bits line 555
  70. theorem OAI.BinPackingGap.BinaryArithmetic.size_monus_le line 559
  71. theorem OAI.BinPackingGap.BinaryArithmetic.monus_bits_length line 562
  72. def OAI.BinPackingGap.UnaryToBinaryMachine.increment line 574
  73. theorem OAI.BinPackingGap.UnaryToBinaryMachine.increment_ne_nil line 579
  74. theorem OAI.BinPackingGap.UnaryToBinaryMachine.bitValue_increment line 584
  75. theorem OAI.BinPackingGap.UnaryToBinaryMachine.canonical_increment line 592
  76. theorem OAI.BinPackingGap.UnaryToBinaryMachine.increment_bits line 603
  77. def OAI.BinPackingGap.UnaryToBinaryMachine.incrementCost line 607
  78. theorem OAI.BinPackingGap.UnaryToBinaryMachine.incrementCost_le line 612
  79. theorem OAI.BinPackingGap.UnaryToBinaryMachine.size_le_self line 620
  80. def OAI.BinPackingGap.UnaryToBinaryMachine.steps line 624
  81. theorem OAI.BinPackingGap.UnaryToBinaryMachine.steps_le line 628
  82. abbrev OAI.BinPackingGap.UnaryToBinaryMachine.Alphabet line 640
  83. abbrev OAI.BinPackingGap.UnaryToBinaryMachine.State line 641
  84. inductive OAI.BinPackingGap.UnaryToBinaryMachine.Label line 643
  85. abbrev OAI.BinPackingGap.UnaryToBinaryMachine.Label.enumList line 647
  86. theorem OAI.BinPackingGap.UnaryToBinaryMachine.Label.enumList_getElem?_ctorIdx_eq line 649
  87. theorem OAI.BinPackingGap.UnaryToBinaryMachine.Label.enumList_nodup line 653
  88. instance OAI.BinPackingGap.UnaryToBinaryMachine.(instance at line 655) line 655
  89. def OAI.BinPackingGap.UnaryToBinaryMachine.finish line 661
  90. def OAI.BinPackingGap.UnaryToBinaryMachine.instruction line 665
  91. def OAI.BinPackingGap.UnaryToBinaryMachine.tapes line 677
  92. theorem OAI.BinPackingGap.UnaryToBinaryMachine.tapes_source line 685
  93. theorem OAI.BinPackingGap.UnaryToBinaryMachine.tapes_output line 690
  94. theorem OAI.BinPackingGap.UnaryToBinaryMachine.tapes_scratch line 694
  95. theorem OAI.BinPackingGap.UnaryToBinaryMachine.tapes_other line 698
  96. theorem OAI.BinPackingGap.UnaryToBinaryMachine.update_source line 704
  97. theorem OAI.BinPackingGap.UnaryToBinaryMachine.update_output line 717
  98. theorem OAI.BinPackingGap.UnaryToBinaryMachine.update_scratch line 727
  99. theorem OAI.BinPackingGap.UnaryToBinaryMachine.scanStep line 739
  100. theorem OAI.BinPackingGap.UnaryToBinaryMachine.carryStep_nil line 752
  101. theorem OAI.BinPackingGap.UnaryToBinaryMachine.carryStep_false line 763
  102. theorem OAI.BinPackingGap.UnaryToBinaryMachine.carryStep_true line 774
  103. theorem OAI.BinPackingGap.UnaryToBinaryMachine.restoreTrace line 786
  104. theorem OAI.BinPackingGap.UnaryToBinaryMachine.oneStepTrace line 804
  105. theorem OAI.BinPackingGap.UnaryToBinaryMachine.joinTrace line 809
  106. theorem OAI.BinPackingGap.UnaryToBinaryMachine.incrementTrace line 814
  107. theorem OAI.BinPackingGap.UnaryToBinaryMachine.convertTrace line 854
  108. def OAI.BinPackingGap.UnaryToBinaryMachine.convertInTime line 881
  109. abbrev OAI.BinPackingGap.BinaryAddMachine.Alphabet line 902
  110. abbrev OAI.BinPackingGap.BinaryAddMachine.State line 903
  111. def OAI.BinPackingGap.BinaryAddMachine.state line 907
  112. def OAI.BinPackingGap.BinaryAddMachine.clean line 910
  113. def OAI.BinPackingGap.BinaryAddMachine.exitAt line 914
  114. def OAI.BinPackingGap.BinaryAddMachine.finish line 919
  115. def OAI.BinPackingGap.BinaryAddMachine.addLoop line 922
  116. def OAI.BinPackingGap.BinaryAddMachine.tapes line 934
  117. theorem OAI.BinPackingGap.BinaryAddMachine.tapes_left line 942
  118. theorem OAI.BinPackingGap.BinaryAddMachine.tapes_right line 947
  119. theorem OAI.BinPackingGap.BinaryAddMachine.tapes_output line 951
  120. theorem OAI.BinPackingGap.BinaryAddMachine.tapes_other line 954
  121. theorem OAI.BinPackingGap.BinaryAddMachine.update_left line 960
  122. theorem OAI.BinPackingGap.BinaryAddMachine.update_right line 973
  123. theorem OAI.BinPackingGap.BinaryAddMachine.update_output line 983
  124. theorem OAI.BinPackingGap.BinaryAddMachine.step_done line 995
  125. theorem OAI.BinPackingGap.BinaryAddMachine.step_more line 1006
  126. theorem OAI.BinPackingGap.BinaryAddMachine.addTrace line 1028
  127. def OAI.BinPackingGap.BinaryAddMachine.addInTime line 1069
  128. def OAI.BinPackingGap.BinaryAddMachine.addNatInTime line 1080
  129. abbrev OAI.BinPackingGap.BinaryTallyMachine.Label line 1099
  130. abbrev OAI.BinPackingGap.BinaryTallyMachine.Alphabet line 1100
  131. def OAI.BinPackingGap.BinaryTallyMachine.instruction line 1104
  132. theorem OAI.BinPackingGap.BinaryTallyMachine.tallyTrace line 1109
  133. theorem OAI.BinPackingGap.BinaryTallyMachine.tally_steps_le line 1124
  134. def OAI.BinPackingGap.BinaryTallyMachine.tallyInTime line 1129
  135. theorem OAI.BinPackingGap.BinaryTallyMachine.joinPlainTrace line 1146
  136. theorem OAI.BinPackingGap.BinaryTallyMachine.stepAsPlainTrace line 1150
  137. theorem OAI.BinPackingGap.BinaryTallyMachine.plainScanEmpty line 1153
  138. theorem OAI.BinPackingGap.BinaryTallyMachine.plainConvertTrace line 1175
  139. theorem OAI.BinPackingGap.BinaryTallyMachine.plainTallyTrace line 1209
  140. def OAI.BinPackingGap.BinaryTallyMachine.plainTallyInTime line 1224
  141. def OAI.BinPackingGap.BinaryTallyMachine.plainTallyFromTapesInTime line 1241
  142. theorem OAI.BinPackingGap.BinaryTallyMachine.result_other line 1273
  143. def OAI.BinPackingGap.BinaryTallyMachine.machine line 1279
  144. def OAI.BinPackingGap.BinaryTallyMachine.configuration line 1290
  145. theorem OAI.BinPackingGap.BinaryTallyMachine.initList_eq line 1294
  146. theorem OAI.BinPackingGap.BinaryTallyMachine.haltList_eq line 1301
  147. theorem OAI.BinPackingGap.BinaryTallyMachine.machineTrace line 1308
  148. def OAI.BinPackingGap.BinaryTallyMachine.outputsInTime line 1318
  149. def OAI.BinPackingGap.BinaryTallyMachine.computableInPolyTime line 1324
  150. theorem OAI.BinPackingGap.BinaryTallyMachine.machine_finiteAlphabet line 1338