OAI/Computability/DeterministicSum/NewtonCommands.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Structured Newton transform commands and memory frames.

  1. def OAI.DeterministicThreeSum.Structured.copyPrefix line 12
  2. def OAI.DeterministicThreeSum.Structured.patched line 16
  3. lemma OAI.DeterministicThreeSum.Structured.patched_zero line 19
  4. lemma OAI.DeterministicThreeSum.Structured.patched_succ line 22
  5. lemma OAI.DeterministicThreeSum.Structured.copyPrefix_correct line 31
  6. lemma OAI.DeterministicThreeSum.Structured.copyPrefix_writes line 53
  7. lemma OAI.DeterministicThreeSum.Structured.protected_frame line 64
  8. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.context line 75
  9. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.saveBanks line 78
  10. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.savedBanks line 81
  11. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.saveBanks_correct line 83
  12. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.degreeSources line 91
  13. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.degreeValues line 95
  14. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.degreeSetup_correct line 98
  15. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.tensorSources line 110
  16. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.tensorValues line 115
  17. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.tensorValues_environment line 118
  18. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.tensorSetup_correct line 122
  19. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.command line 138
  20. def OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.filtered line 142
  21. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.banks_twice line 145
  22. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.tensorStride_le line 148
  23. lemma OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.initialCount_le line 153
  24. theorem OAI.DeterministicThreeSum.Structured.Indexed.NewtonPass.command_correct line 161