OAI/Computability/PerfectCompleteness/Foundations/OriginalWholeCut.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.OriginalWholeCut.Values line 18
  2. abbrev OAI.PerfectCompleteness.OriginalWholeCut.ChildArrays line 22
  3. abbrev OAI.PerfectCompleteness.OriginalWholeCut.BelowArrays line 26
  4. abbrev OAI.PerfectCompleteness.OriginalWholeCut.Record line 30
  5. def OAI.PerfectCompleteness.OriginalWholeCut.belowEvaluate line 34
  6. def OAI.PerfectCompleteness.OriginalWholeCut.reconstructBuckets line 40
  7. theorem OAI.PerfectCompleteness.OriginalWholeCut.reconstructBuckets_original line 51
  8. def OAI.PerfectCompleteness.OriginalWholeCut.reconstruct line 68
  9. def OAI.PerfectCompleteness.OriginalWholeCut.reconstructRecord line 84
  10. def OAI.PerfectCompleteness.OriginalWholeCut.readRecord line 89
  11. theorem OAI.PerfectCompleteness.OriginalWholeCut.reconstruct_original line 100
  12. def OAI.PerfectCompleteness.OriginalWholeCut.callNumbering line 123
  13. def OAI.PerfectCompleteness.OriginalWholeCut.numberedValues line 129
  14. def OAI.PerfectCompleteness.OriginalWholeCut.reconstructNumbered line 134
  15. theorem OAI.PerfectCompleteness.OriginalWholeCut.reconstructNumbered_numberedValues line 141
  16. theorem OAI.PerfectCompleteness.OriginalWholeCut.reconstructNumbered_original line 152