OAI/Computability/DeterministicSum/IndexedLoops.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Indexed kernels and memory-preserving iteration.

  1. def OAI.DeterministicThreeSum.Structured.written line 11
  2. lemma OAI.DeterministicThreeSum.Structured.written_next line 14
  3. lemma OAI.DeterministicThreeSum.Structured.written_zero line 25
  4. lemma OAI.DeterministicThreeSum.Structured.written_outside line 30
  5. def OAI.DeterministicThreeSum.Structured.indexedLoop line 34
  6. theorem OAI.DeterministicThreeSum.Structured.indexedLoop_correct line 38
  7. def OAI.DeterministicThreeSum.Structured.Indexed.Scalar.reads line 87
  8. lemma OAI.DeterministicThreeSum.Structured.Indexed.Scalar.memory_congr line 93
  9. def OAI.DeterministicThreeSum.Structured.Indexed.kernelBody line 115
  10. def OAI.DeterministicThreeSum.Structured.Indexed.kernel line 119
  11. theorem OAI.DeterministicThreeSum.Structured.Indexed.kernel_correct line 122