OAI/Computability/PerfectCompleteness/Decoding/LowerCutBucketLocality.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.LowerCutBucketLocality.F2 line 17
  2. def OAI.PerfectCompleteness.LowerCutBucketLocality.rootBuckets line 21
  3. def OAI.PerfectCompleteness.LowerCutBucketLocality.buckets line 32
  4. theorem OAI.PerfectCompleteness.LowerCutBucketLocality.buckets_congr_otherCalls line 44
  5. theorem OAI.PerfectCompleteness.LowerCutBucketLocality.buckets_splitTape line 79
  6. def OAI.PerfectCompleteness.LowerCutBucketLocality.knownBuckets line 102
  7. def OAI.PerfectCompleteness.LowerCutBucketLocality.knownBucketsOfComplement line 112
  8. theorem OAI.PerfectCompleteness.LowerCutBucketLocality.knownBuckets_merge line 123
  9. theorem OAI.PerfectCompleteness.LowerCutBucketLocality.knownBuckets_eq_complement line 145
  10. theorem OAI.PerfectCompleteness.LowerCutBucketLocality.knownBucketsAtNode_eq_complement line 165
  11. theorem OAI.PerfectCompleteness.LowerCutBucketLocality.knownBucketsAtNode_join line 187
  12. theorem OAI.PerfectCompleteness.LowerCutBucketLocality.knownBucketsAtNode_erase_eq line 205
  13. theorem OAI.PerfectCompleteness.LowerCutBucketLocality.knownBucketsAtNode_assemble_splitTape line 222
  14. theorem OAI.PerfectCompleteness.LowerCutBucketLocality.knownBucketsAtNode_assemble line 243