OAI/Computability/DeterministicSum/PrunedCache.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Paid prefix-key setup and complete sparse cache production.

  1. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.seedKeys line 12
  2. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.seeded line 17
  3. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.seedKeys_correct line 20
  4. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.seeded_stored line 28
  5. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.seeded_regs line 32
  6. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.seeded_frame line 38
  7. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.keysHandoff line 44
  8. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.keyHanded line 47
  9. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.keysHandoff_correct line 50
  10. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.prunedKeys line 59
  11. theorem OAI.DeterministicThreeSum.Structured.Indexed.Cache.prunedKeys_correct line 62
  12. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.keyList line 126
  13. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.keyAt line 127
  14. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.keyAt_eq line 129
  15. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.keyAt_bound line 132
  16. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.keyAt_stored line 140
  17. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.frame_interval line 144
  18. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.keys_batch_regs line 150
  19. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.prunedBatch line 167
  20. theorem OAI.DeterministicThreeSum.Structured.Indexed.Cache.prunedBatch_correct line 170