OAI/Computability/BinPacking/Arithmetic/BinaryToTallyMachine.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.BinaryRegisterStructured.code line 17
  2. theorem OAI.BinPackingGap.BinaryRegisterStructured.exec line 24
  3. theorem OAI.BinPackingGap.BinaryRegisterStructured.exec_polynomial line 58
  4. theorem OAI.BinPackingGap.BinaryRegisterStructured.final_width line 72
  5. theorem OAI.BinPackingGap.RegisterFrameEmission.external_update line 93
  6. def OAI.BinPackingGap.RegisterFrameEmission.code line 108
  7. theorem OAI.BinPackingGap.RegisterFrameEmission.exec line 112
  8. inductive OAI.BinPackingGap.BinaryToTallyMachine.Reg line 168
  9. instance OAI.BinPackingGap.BinaryToTallyMachine.(instance at line 172) line 172
  10. abbrev OAI.BinPackingGap.BinaryToTallyMachine.State line 176
  11. def OAI.BinPackingGap.BinaryToTallyMachine.initial line 178
  12. def OAI.BinPackingGap.BinaryToTallyMachine.running line 182
  13. def OAI.BinPackingGap.BinaryToTallyMachine.subtractOperands line 188
  14. def OAI.BinPackingGap.BinaryToTallyMachine.prepareCommands line 196
  15. def OAI.BinPackingGap.BinaryToTallyMachine.decrementCommands line 199
  16. def OAI.BinPackingGap.BinaryToTallyMachine.finishCommands line 203
  17. theorem OAI.BinPackingGap.BinaryToTallyMachine.prepare_ready line 205
  18. theorem OAI.BinPackingGap.BinaryToTallyMachine.prepare_result line 208
  19. theorem OAI.BinPackingGap.BinaryToTallyMachine.prepare_budget line 214
  20. theorem OAI.BinPackingGap.BinaryToTallyMachine.decrement_ready line 219
  21. theorem OAI.BinPackingGap.BinaryToTallyMachine.decrement_result line 223
  22. theorem OAI.BinPackingGap.BinaryToTallyMachine.decrement_budget line 229
  23. theorem OAI.BinPackingGap.BinaryToTallyMachine.finish_ready line 236
  24. theorem OAI.BinPackingGap.BinaryToTallyMachine.finish_result line 239
  25. theorem OAI.BinPackingGap.BinaryToTallyMachine.finish_budget line 245
  26. def OAI.BinPackingGap.BinaryToTallyMachine.guard line 250
  27. def OAI.BinPackingGap.BinaryToTallyMachine.more line 253
  28. def OAI.BinPackingGap.BinaryToTallyMachine.reset line 255
  29. def OAI.BinPackingGap.BinaryToTallyMachine.body line 258
  30. def OAI.BinPackingGap.BinaryToTallyMachine.loop line 262
  31. def OAI.BinPackingGap.BinaryToTallyMachine.code line 265
  32. theorem OAI.BinPackingGap.BinaryToTallyMachine.bits_succ_nonempty line 269
  33. theorem OAI.BinPackingGap.BinaryToTallyMachine.guard_more line 275
  34. theorem OAI.BinPackingGap.BinaryToTallyMachine.guard_zero line 286
  35. theorem OAI.BinPackingGap.BinaryToTallyMachine.registerTapes_update_external line 293
  36. theorem OAI.BinPackingGap.BinaryToTallyMachine.body_exec line 307
  37. theorem OAI.BinPackingGap.BinaryToTallyMachine.replicate_append_true line 340
  38. theorem OAI.BinPackingGap.BinaryToTallyMachine.loop_exec line 346
  39. def OAI.BinPackingGap.BinaryToTallyMachine.runtimeBound line 381
  40. theorem OAI.BinPackingGap.BinaryToTallyMachine.exec line 383
  41. theorem OAI.BinPackingGap.BinaryToTallyMachine.exec_from_tapes line 411