OAI/Computability/PerfectCompleteness/Decoding/FixedStoppedDecoderContext.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderContext.Prefixes line 24
  2. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.upperPath line 28
  3. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.lowerPath line 32
  4. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.upper line 36
  5. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.lower line 39
  6. theorem OAI.PerfectCompleteness.FixedStoppedDecoderContext.upper_height line 44
  7. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.prefixLaw line 48
  8. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderContext.OutsideQuestions line 56
  9. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderContext.Exterior line 60
  10. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderContext.Advice line 65
  11. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderContext.Directions line 69
  12. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderContext.Fiber line 71
  13. abbrev OAI.PerfectCompleteness.FixedStoppedDecoderContext.Context line 76
  14. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.directionLaw line 81
  15. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.fiberLaw line 85
  16. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.law line 92
  17. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.upperNode line 98
  18. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.lowerIndex line 100
  19. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.geometry line 102
  20. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.advice line 109
  21. def OAI.PerfectCompleteness.FixedStoppedDecoderContext.direction line 114
  22. theorem OAI.PerfectCompleteness.FixedStoppedDecoderContext.row_count line 124
  23. theorem OAI.PerfectCompleteness.FixedStoppedDecoderContext.advice_marginal line 129