OAI/Computability/PerfectCompleteness/Foundations/WholeReplaySubtreeLemmas.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.WholeReplaySubtree.F2 line 17
  2. def OAI.PerfectCompleteness.WholeReplaySubtree.extract line 21
  3. theorem OAI.PerfectCompleteness.WholeReplaySubtree.extract_refl line 31
  4. theorem OAI.PerfectCompleteness.WholeReplaySubtree.extract_step line 37
  5. theorem OAI.PerfectCompleteness.WholeReplaySubtree.restrictArrays_evaluateArrays line 44
  6. def OAI.PerfectCompleteness.WholeReplaySubtree.restrictBlocks line 63
  7. theorem OAI.PerfectCompleteness.WholeReplaySubtree.restrictBlocks_joint line 70
  8. theorem OAI.PerfectCompleteness.WholeReplaySubtree.evaluate_extract line 84
  9. def OAI.PerfectCompleteness.WholeReplaySubtree.rootBuckets line 111
  10. theorem OAI.PerfectCompleteness.WholeReplaySubtree.rootBuckets_step line 120
  11. def OAI.PerfectCompleteness.WholeReplaySubtree.buckets line 128
  12. def OAI.PerfectCompleteness.WholeReplaySubtree.knownBuckets line 136
  13. def OAI.PerfectCompleteness.WholeReplaySubtree.knownBucketsAtNode line 144
  14. theorem OAI.PerfectCompleteness.WholeReplaySubtree.knownBucketsAtNode_apply line 152
  15. abbrev OAI.PerfectCompleteness.WholeCutSubtree.F2 line 177
  16. def OAI.PerfectCompleteness.WholeCutSubtree.extract line 181
  17. theorem OAI.PerfectCompleteness.WholeCutSubtree.extract_refl line 190
  18. theorem OAI.PerfectCompleteness.WholeCutSubtree.extract_step line 195
  19. theorem OAI.PerfectCompleteness.WholeCutSubtree.erase_extract line 202
  20. theorem OAI.PerfectCompleteness.WholeCutSubtree.zero_extract line 219
  21. theorem OAI.PerfectCompleteness.WholeCutSubtree.collapse_extract line 233
  22. def OAI.PerfectCompleteness.WholeCutSubtree.rootBuckets line 247
  23. def OAI.PerfectCompleteness.WholeCutSubtree.knownBuckets line 257
  24. theorem OAI.PerfectCompleteness.WholeCutSubtree.rootBuckets_erase line 266
  25. theorem OAI.PerfectCompleteness.WholeCutSubtree.knownBuckets_erase line 281
  26. theorem OAI.PerfectCompleteness.WholeCutSubtree.knownBuckets_eq_original line 296
  27. def OAI.PerfectCompleteness.WholeCutSubtree.knownBucketsAtNode line 320
  28. theorem OAI.PerfectCompleteness.WholeCutSubtree.knownBucketsAtNode_erase line 328
  29. theorem OAI.PerfectCompleteness.WholeCutSubtree.knownBucketsAtNode_eq_ownInput line 341