OAI/Computability/PerfectCompleteness/Construction/StoppedProjectedBucketIndex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.StoppedProjectedBucketIndex.Base line 18
  2. def OAI.PerfectCompleteness.StoppedProjectedBucketIndex.baseOf line 21
  3. def OAI.PerfectCompleteness.StoppedProjectedBucketIndex.withDirections line 26
  4. theorem OAI.PerfectCompleteness.StoppedProjectedBucketIndex.baseOf_withDirections line 33
  5. theorem OAI.PerfectCompleteness.StoppedProjectedBucketIndex.withDirections_baseOf line 38
  6. def OAI.PerfectCompleteness.StoppedProjectedBucketIndex.defaultDirections line 43
  7. def OAI.PerfectCompleteness.StoppedProjectedBucketIndex.baseLaw line 48
  8. abbrev OAI.PerfectCompleteness.StoppedProjectedBucketIndex.key line 61
  9. abbrev OAI.PerfectCompleteness.StoppedProjectedBucketIndex.Tape line 64
  10. def OAI.PerfectCompleteness.StoppedProjectedBucketIndex.tapeLaw line 70
  11. theorem OAI.PerfectCompleteness.StoppedProjectedBucketIndex.projectedSlots_eq line 77
  12. theorem OAI.PerfectCompleteness.StoppedProjectedBucketIndex.expectation_coordinate line 84