OAI/Combinatorics/LowSpaceSubsetSum/Storage/ComputedFuelCells.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Constant-state loop limits and their live domain scans

The length, binomial, and doubling loops retain scalar accumulators only. No leaf occurrence is enumerated. The three domain lists are retained through the scalar computation and released when the leaf limit returns.

  1. def OAI.LowSpaceSubsetSum.ComputedFuelCells.lengthLoop line 17
  2. theorem OAI.LowSpaceSubsetSum.ComputedFuelCells.lengthLoop_formula line 21
  3. def OAI.LowSpaceSubsetSum.ComputedFuelCells.powerLoop line 29
  4. theorem OAI.LowSpaceSubsetSum.ComputedFuelCells.powerLoop_formula line 33
  5. def OAI.LowSpaceSubsetSum.ComputedFuelCells.chooseAcc line 41
  6. theorem OAI.LowSpaceSubsetSum.ComputedFuelCells.chooseAcc_value line 45
  7. theorem OAI.LowSpaceSubsetSum.ComputedFuelCells.chooseAcc_cells line 51
  8. def OAI.LowSpaceSubsetSum.ComputedFuelCells.choose line 57
  9. theorem OAI.LowSpaceSubsetSum.ComputedFuelCells.choose_value line 60
  10. theorem OAI.LowSpaceSubsetSum.ComputedFuelCells.choose_cells line 66
  11. def OAI.LowSpaceSubsetSum.ComputedFuelCells.leaf line 72
  12. theorem OAI.LowSpaceSubsetSum.ComputedFuelCells.leaf_value line 87
  13. theorem OAI.LowSpaceSubsetSum.ComputedFuelCells.leaf_cells line 94
  14. def OAI.LowSpaceSubsetSum.ComputedFuelCells.run line 105
  15. theorem OAI.LowSpaceSubsetSum.ComputedFuelCells.run_value line 114
  16. theorem OAI.LowSpaceSubsetSum.ComputedFuelCells.run_cells line 118