OAI/Computability/DeterministicSum/AxisMaps.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Finite coordinate transforms, address bounds and tensor passes.

  1. def OAI.DeterministicThreeSum.Structured.Indexed.Scalar.sum line 12
  2. lemma OAI.DeterministicThreeSum.Structured.Indexed.Scalar.sum_value line 16
  3. lemma OAI.DeterministicThreeSum.Structured.Indexed.Scalar.sum_valid line 25
  4. lemma OAI.DeterministicThreeSum.Structured.Indexed.Scalar.sum_reads line 32
  5. lemma OAI.DeterministicThreeSum.Structured.Indexed.Scalar.sum_cast_value line 44
  6. abbrev OAI.DeterministicThreeSum.Structured.Indexed.Axis.idx line 51
  7. abbrev OAI.DeterministicThreeSum.Structured.Indexed.Axis.src line 52
  8. abbrev OAI.DeterministicThreeSum.Structured.Indexed.Axis.coeff line 53
  9. abbrev OAI.DeterministicThreeSum.Structured.Indexed.Axis.stride line 54
  10. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.outer line 56
  11. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.digit line 57
  12. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.suffix line 58
  13. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.inputAddress line 60
  14. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.coeffAddress line 62
  15. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.term line 65
  16. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.row line 66
  17. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.pass line 67
  18. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.sourceIndex line 69
  19. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.coefficientIndex line 70
  20. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.environment line 72
  21. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.inputAddress_value line 75
  22. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.coeffAddress_value line 78
  23. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.quotient_bounds line 82
  24. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.sourceIndex_bound line 89
  25. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.coefficientIndex_bound line 97
  26. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.addresses_valid line 110
  27. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.row_valid line 139
  28. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.row_value line 159
  29. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.row_reads_outside line 173
  30. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.environment_update line 191
  31. theorem OAI.DeterministicThreeSum.Structured.Indexed.Axis.pass_correct line 197
  32. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.mapValue line 249
  33. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.mapValue_lt line 252
  34. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.mapValue_cast line 255
  35. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.pass_exact line 260
  36. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.tensorUpdate line 283
  37. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.tensorUpdateState line 290
  38. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.tensorUpdate_correct line 294
  39. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.tensorBody line 311
  40. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.tensorCommand line 312
  41. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.tensorValue line 314
  42. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.banks line 318
  43. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.banks_zero line 320
  44. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.banks_succ line 321
  45. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.tensorStride line 330
  46. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.tensorStride_div line 334
  47. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.stage_lengths line 340
  48. theorem OAI.DeterministicThreeSum.Structured.Indexed.Axis.tensorCommand_correct line 354
  49. def OAI.DeterministicThreeSum.Structured.Indexed.Axis.boxIndex line 450
  50. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.boxIndex_lt line 452
  51. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.boxIndex_parts line 459
  52. lemma OAI.DeterministicThreeSum.Structured.Indexed.Axis.mapValue_box line 470
  53. theorem OAI.DeterministicThreeSum.Structured.Indexed.Axis.pass_box_correct line 480