OAI/Computability/BinPacking/Arithmetic/PackingRegisterFrame.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingGap.BinaryRegisterProgram.Operands line 11
  2. def OAI.BinPackingGap.BinaryRegisterProgram.addSlots line 21
  3. theorem OAI.BinPackingGap.BinaryRegisterProgram.addSlots_zero line 32
  4. theorem OAI.BinPackingGap.BinaryRegisterProgram.addSlots_one line 35
  5. theorem OAI.BinPackingGap.BinaryRegisterProgram.addSlots_two line 38
  6. theorem OAI.BinPackingGap.BinaryRegisterProgram.addSlots_three line 41
  7. theorem OAI.BinPackingGap.BinaryRegisterProgram.addSlots_four line 44
  8. theorem OAI.BinPackingGap.BinaryRegisterProgram.addSlots_five line 47
  9. theorem OAI.BinPackingGap.BinaryRegisterProgram.addSlots_six line 50
  10. def OAI.BinPackingGap.BinaryRegisterProgram.mulSlots line 53
  11. theorem OAI.BinPackingGap.BinaryRegisterProgram.mulSlots_zero line 64
  12. theorem OAI.BinPackingGap.BinaryRegisterProgram.mulSlots_one line 67
  13. theorem OAI.BinPackingGap.BinaryRegisterProgram.mulSlots_two line 70
  14. theorem OAI.BinPackingGap.BinaryRegisterProgram.mulSlots_three line 73
  15. theorem OAI.BinPackingGap.BinaryRegisterProgram.mulSlots_four line 76
  16. theorem OAI.BinPackingGap.BinaryRegisterProgram.mulSlots_five line 79
  17. theorem OAI.BinPackingGap.BinaryRegisterProgram.mulSlots_six line 82
  18. theorem OAI.BinPackingGap.BinaryRegisterProgram.mulSlots_seven line 85
  19. theorem OAI.BinPackingGap.BinaryRegisterProgram.mulSlots_eight line 88
  20. def OAI.BinPackingGap.BinaryRegisterProgram.registerWords line 91
  21. theorem OAI.BinPackingGap.BinaryRegisterProgram.registerWords_reg line 95
  22. theorem OAI.BinPackingGap.BinaryRegisterProgram.registerWords_scratch line 98
  23. def OAI.BinPackingGap.BinaryRegisterProgram.registerTapes line 101
  24. theorem OAI.BinPackingGap.BinaryRegisterProgram.registerTapes_slot line 107
  25. theorem OAI.BinPackingGap.BinaryRegisterProgram.registerTapes_reg line 115
  26. theorem OAI.BinPackingGap.BinaryRegisterProgram.registerTapes_scratch line 120
  27. theorem OAI.BinPackingGap.BinaryRegisterProgram.registerTapes_other line 125
  28. theorem OAI.BinPackingGap.BinaryRegisterProgram.registerTapes_update line 130
  29. theorem OAI.BinPackingGap.BinaryRegisterProgram.registerTapes_mul_workspace line 151
  30. theorem OAI.BinPackingGap.BinaryRegisterProgram.registerTapes_add_workspace line 157
  31. def OAI.BinPackingGap.PackingRegisterFrame.withScratch line 173
  32. def OAI.BinPackingGap.PackingRegisterFrame.localSlots line 183
  33. theorem OAI.BinPackingGap.PackingRegisterFrame.localSlots_reg line 186
  34. theorem OAI.BinPackingGap.PackingRegisterFrame.localSlots_scratch line 190
  35. theorem OAI.BinPackingGap.PackingRegisterFrame.registerTapes_eq_self line 194
  36. theorem OAI.BinPackingGap.PackingRegisterFrame.restrict line 204
  37. theorem OAI.BinPackingGap.PackingRegisterFrame.replace line 212
  38. theorem OAI.BinPackingGap.PackingRegisterFrame.external_update line 246