OAI/Computability/DepthThree/SparseTree.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.SparseEligible line 17
  2. def OAI.DepthThreeLowerBound.SparseTerminal line 20
  3. theorem OAI.DepthThreeLowerBound.sparseTerminal_of_not_eligible line 23
  4. structure OAI.DepthThreeLowerBound.SparseSelection line 27
  5. def OAI.DepthThreeLowerBound.sparseSelect line 33
  6. def OAI.DepthThreeLowerBound.SparseSelection.branch line 45
  7. def OAI.DepthThreeLowerBound.SparseSelection.step line 48
  8. def OAI.DepthThreeLowerBound.SparseSelection.label line 56
  9. theorem OAI.DepthThreeLowerBound.SparseSelection.branch_valid line 59
  10. theorem OAI.DepthThreeLowerBound.SparseSelection.branch_eval_imp line 62
  11. def OAI.DepthThreeLowerBound.SparsePath.prepend line 78
  12. theorem OAI.DepthThreeLowerBound.SparsePath.length_prepend line 83
  13. theorem OAI.DepthThreeLowerBound.SparsePath.processed_prepend line 90
  14. theorem OAI.DepthThreeLowerBound.SparsePath.petalSteps_prepend line 98
  15. structure OAI.DepthThreeLowerBound.SparseTreeResult line 108
  16. def OAI.DepthThreeLowerBound.SparseTreeResult.stop line 124
  17. def OAI.DepthThreeLowerBound.SparseTreeResult.join line 143
  18. def OAI.DepthThreeLowerBound.SparseTreeResult.build line 245
  19. def OAI.DepthThreeLowerBound.sparseTreeFuel line 259
  20. def OAI.DepthThreeLowerBound.sparseTree line 262
  21. theorem OAI.DepthThreeLowerBound.sparseTree_terminal line 266
  22. theorem OAI.DepthThreeLowerBound.sparseTree_stream_length line 281
  23. theorem OAI.DepthThreeLowerBound.sparseTree_stream_ones line 290