OAI/Computability/DeterministicSum/DegreeFilter.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Charged digit-degree filters and finite-memory output bounds.

  1. def OAI.DeterministicThreeSum.Structured.Indexed.DigitSum.value line 11
  2. lemma OAI.DeterministicThreeSum.Structured.Indexed.DigitSum.value_zero line 15
  3. lemma OAI.DeterministicThreeSum.Structured.Indexed.DigitSum.value_le line 17
  4. def OAI.DeterministicThreeSum.Structured.Indexed.DigitSum.step line 27
  5. def OAI.DeterministicThreeSum.Structured.Indexed.DigitSum.loop line 31
  6. def OAI.DeterministicThreeSum.Structured.Indexed.DigitSum.stepState line 33
  7. lemma OAI.DeterministicThreeSum.Structured.Indexed.DigitSum.step_correct line 35
  8. theorem OAI.DeterministicThreeSum.Structured.Indexed.DigitSum.loop_correct line 43
  9. def OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.memory line 79
  10. lemma OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.memory_zero line 82
  11. lemma OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.memory_succ line 85
  12. def OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.setup line 96
  13. def OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.erase line 98
  14. def OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.conditional line 100
  15. def OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.body line 101
  16. def OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.loop line 103
  17. def OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.command line 104
  18. lemma OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.setup_correct line 106
  19. lemma OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.erase_correct line 113
  20. lemma OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.conditional_correct line 120
  21. lemma OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.body_correct line 133
  22. theorem OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.command_correct line 173
  23. lemma OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.memory_entry line 214
  24. lemma OAI.DeterministicThreeSum.Structured.Indexed.DegreeFilter.memory_outside line 219