OAI/Computability/DeterministicSum/MatrixDown.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Uniform downward matrix recursion and address-capacity invariants.

  1. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.update line 11
  2. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.updated line 21
  3. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.ceil_eq line 26
  4. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.update_correct line 31
  5. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.body line 55
  6. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.loop line 56
  7. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.value line 58
  8. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.capacity line 63
  9. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.finalCount line 68
  10. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.capacity_output line 77
  11. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.capacity_input line 83
  12. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.batch_pos line 94
  13. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.batch_le line 101
  14. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.loop_correct line 105
  15. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.leftLeaves line 210
  16. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.value_leftLeaves line 215
  17. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.left_loop_correct line 234
  18. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.rightLeaves line 275
  19. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixDown.value_rightLeaves line 280