OAI/Computability/DeterministicSum/CacheRows.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Source-identical evaluated coefficient rows and complete charged batch caching.

  1. theorem OAI.DeterministicThreeSum.Structured.Indexed.Cache.Uvalue_source line 15
  2. theorem OAI.DeterministicThreeSum.Structured.Indexed.Cache.Wvalue_source line 38
  3. def OAI.DeterministicThreeSum.Structured.copyStep line 73
  4. theorem OAI.DeterministicThreeSum.Structured.copyStep_correct line 77
  5. def OAI.DeterministicThreeSum.Structured.copyPass line 96
  6. theorem OAI.DeterministicThreeSum.Structured.copyPass_correct line 98
  7. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchBase line 131
  8. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchBase_ge line 134
  9. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchBase_gt line 135
  10. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchValues line 139
  11. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchSources line 145
  12. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchLowValues line 152
  13. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchSetup line 157
  14. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchSetup_correct line 159
  15. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.loadKey line 182
  16. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.loadKey_correct line 187
  17. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.rowCopySetup line 201
  18. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.rowCopySetup_correct line 206
  19. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.storeRow line 224
  20. theorem OAI.DeterministicThreeSum.Structured.Indexed.Cache.storeRow_correct line 227
  21. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.prepareRow line 305
  22. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.prepared line 307
  23. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.prepareRow_correct line 310
  24. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.prepared_low line 328
  25. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.prepared_frame line 336
  26. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchBody line 345
  27. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.outside_separated line 348
  28. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchValues_nonzero line 351
  29. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchValues_bound line 358
  30. theorem OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchBody_correct line 371
  31. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchCtx_bounds line 437
  32. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.readonly_cache line 456
  33. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchCommand line 470
  34. theorem OAI.DeterministicThreeSum.Structured.Indexed.Cache.batchCommand_correct line 474