OAI/Computability/DeterministicSum/MatrixUp.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Return-count stacks and uniform upward matrix recursion.

  1. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixLayout.combine_level_correct line 13
  2. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixTrace.body line 57
  3. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixTrace.command line 64
  4. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixTrace.next line 66
  5. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixTrace.body_correct line 71
  6. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixTrace.finalCount_succ line 89
  7. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixTrace.command_correct line 95
  8. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.setup line 143
  9. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.prepared line 147
  10. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.setup_correct line 150
  11. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.update line 166
  12. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.updated line 169
  13. lemma OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.update_correct line 172
  14. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.body line 182
  15. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.command line 184
  16. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.body_correct line 187
  17. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.Bounds line 250
  18. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.outputSize line 254
  19. def OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.value line 257
  20. theorem OAI.DeterministicThreeSum.Structured.Indexed.MatrixUp.command_correct line 261