OAI/Computability/PerfectCompleteness/Foundations/StoppedProjectedContext.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.StoppedProjectedContext.Sample line 19
  2. abbrev OAI.PerfectCompleteness.StoppedProjectedContext.SplitSample line 23
  3. def OAI.PerfectCompleteness.StoppedProjectedContext.splitEquiv line 29
  4. theorem OAI.PerfectCompleteness.StoppedProjectedContext.questions_split line 45
  5. theorem OAI.PerfectCompleteness.StoppedProjectedContext.tag_split line 49
  6. theorem OAI.PerfectCompleteness.StoppedProjectedContext.directions_split line 53
  7. theorem OAI.PerfectCompleteness.StoppedProjectedContext.stoppedPath_split line 57
  8. theorem OAI.PerfectCompleteness.StoppedProjectedContext.lower_split line 64
  9. theorem OAI.PerfectCompleteness.StoppedProjectedContext.fullPath_split_spec line 72
  10. theorem OAI.PerfectCompleteness.StoppedProjectedContext.expectation_split line 94
  11. theorem OAI.PerfectCompleteness.StoppedProjectedContext.split_law line 124