OAI/Computability/DeterministicSum/CacheGather.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Charged index interleaving, coefficient gathering and row evaluation.

  1. def OAI.DeterministicThreeSum.Structured.Indexed.ZipIndex.value line 11
  2. lemma OAI.DeterministicThreeSum.Structured.Indexed.ZipIndex.value_lt line 14
  3. def OAI.DeterministicThreeSum.Structured.Indexed.ZipIndex.step line 26
  4. def OAI.DeterministicThreeSum.Structured.Indexed.ZipIndex.command line 39
  5. def OAI.DeterministicThreeSum.Structured.Indexed.ZipIndex.stepState line 41
  6. def OAI.DeterministicThreeSum.Structured.Indexed.ZipIndex.Regs line 46
  7. lemma OAI.DeterministicThreeSum.Structured.Indexed.ZipIndex.step_correct line 50
  8. theorem OAI.DeterministicThreeSum.Structured.Indexed.ZipIndex.command_correct line 80
  9. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.TailOK line 136
  10. instance OAI.DeterministicThreeSum.Structured.Indexed.Cache.(instance at line 137) line 137
  11. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.loadCoefficient line 138
  12. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.zeroCoefficient line 140
  13. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.tailRead line 141
  14. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.readCoefficient line 143
  15. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.loadCoefficient_correct line 147
  16. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.zeroCoefficient_correct line 158
  17. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.tailRead_correct line 164
  18. theorem OAI.DeterministicThreeSum.Structured.Indexed.Cache.readCoefficient_correct line 185
  19. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.leftIndex line 215
  20. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.rightIndex line 216
  21. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.zipInputs line 218
  22. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.zipValues line 225
  23. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.setupZip line 226
  24. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.setupZip_exact line 228
  25. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.outputWrite line 241
  26. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.outputWrite_correct line 243
  27. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.gathered line 256
  28. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.gatherBody line 262
  29. theorem OAI.DeterministicThreeSum.Structured.Indexed.Cache.gatherBody_correct line 265
  30. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.gatherRow line 322
  31. theorem OAI.DeterministicThreeSum.Structured.Indexed.Cache.gatherRow_correct line 325
  32. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.zipDigit line 377
  33. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.lowCode_parts line 385
  34. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.zipValue_lowCode line 392
  35. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.digitSum_lowCode line 401
  36. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.digitFunction_zip line 409
  37. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.gathered_U line 419
  38. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.gathered_W line 426
  39. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.evaluationSources line 437
  40. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.evaluationSetup line 442
  41. lemma OAI.DeterministicThreeSum.Structured.Indexed.Cache.evaluationSetup_correct line 444
  42. def OAI.DeterministicThreeSum.Structured.Indexed.Cache.evaluateRow line 460
  43. theorem OAI.DeterministicThreeSum.Structured.Indexed.Cache.evaluateRow_correct line 463