OAI/Computability/PerfectCompleteness/Decoding/CleanLeftDecoderLemmas.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PerfectCompleteness.CleanLeftDecoder.Exposed line 22
  2. abbrev OAI.PerfectCompleteness.CleanLeftDecoder.Own line 37
  3. instance OAI.PerfectCompleteness.CleanLeftDecoder.ownFintype line 39
  4. def OAI.PerfectCompleteness.CleanLeftDecoder.slots line 41
  5. def OAI.PerfectCompleteness.CleanLeftDecoder.replay line 44
  6. def OAI.PerfectCompleteness.CleanLeftDecoder.arrays line 48
  7. def OAI.PerfectCompleteness.CleanLeftDecoder.background line 53
  8. def OAI.PerfectCompleteness.CleanLeftDecoder.upperMatrix line 57
  9. def OAI.PerfectCompleteness.CleanLeftDecoder.quotientMatrix line 61
  10. abbrev OAI.PerfectCompleteness.CleanLeftDecoder.QuotientAdvice line 68
  11. def OAI.PerfectCompleteness.CleanLeftDecoder.advice line 73
  12. abbrev OAI.PerfectCompleteness.CleanLeftDecoder.UpperAnswer line 77
  13. instance OAI.PerfectCompleteness.CleanLeftDecoder.upperAnswerFintype line 85
  14. abbrev OAI.PerfectCompleteness.CleanLeftDecoder.Useful line 88
  15. def OAI.PerfectCompleteness.CleanLeftDecoder.law line 95
  16. abbrev OAI.PerfectCompleteness.CleanLeftDecoder.Seed line 101
  17. def OAI.PerfectCompleteness.CleanLeftDecoder.seedLaw line 103
  18. theorem OAI.PerfectCompleteness.CleanLeftDecoder.seedLaw_marginal line 108
  19. theorem OAI.PerfectCompleteness.CleanLeftDecoder.supported_row line 115
  20. theorem OAI.PerfectCompleteness.CleanLeftDecoder.law_valid line 126
  21. theorem OAI.PerfectCompleteness.CleanLeftDecoder.supported_seed_valid line 135
  22. theorem OAI.PerfectCompleteness.CleanLeftDecoder.seedLaw_valid line 148
  23. abbrev OAI.PerfectCompleteness.CleanLeftDecoder.LowerH line 159
  24. abbrev OAI.PerfectCompleteness.CleanLeftDecoder.LowerAnswer line 162
  25. instance OAI.PerfectCompleteness.CleanLeftDecoder.lowerAnswerFintype line 165
  26. def OAI.PerfectCompleteness.CleanLeftDecoder.output line 169
  27. def OAI.PerfectCompleteness.CleanLeftDecoder.form line 173
  28. def OAI.PerfectCompleteness.CleanLeftDecoder.formFamily line 179
  29. def OAI.PerfectCompleteness.CleanLeftDecoder.outputLaw line 184
  30. theorem OAI.PerfectCompleteness.CleanLeftDecoder.seedLaw_output_marginal line 190
  31. theorem OAI.PerfectCompleteness.CleanLeftDecoder.supported_output_normalized line 204
  32. theorem OAI.PerfectCompleteness.CleanLeftDecoder.supported_form_tested_rank line 212
  33. abbrev OAI.PerfectCompleteness.CleanRightDecoder.F2 line 236
  34. def OAI.PerfectCompleteness.CleanRightDecoder.suffix line 242
  35. theorem OAI.PerfectCompleteness.CleanRightDecoder.suffix_proper line 246
  36. def OAI.PerfectCompleteness.CleanRightDecoder.fullPath line 251
  37. abbrev OAI.PerfectCompleteness.CleanRightDecoder.OwnQuestions line 257
  38. def OAI.PerfectCompleteness.CleanRightDecoder.slots line 271
  39. abbrev OAI.PerfectCompleteness.CleanRightDecoder.Record line 278
  40. def OAI.PerfectCompleteness.CleanRightDecoder.replay line 285
  41. def OAI.PerfectCompleteness.CleanRightDecoder.arrays line 291
  42. def OAI.PerfectCompleteness.CleanRightDecoder.exterior line 298
  43. def OAI.PerfectCompleteness.CleanRightDecoder.knownBuckets line 310
  44. def OAI.PerfectCompleteness.CleanRightDecoder.input line 320
  45. theorem OAI.PerfectCompleteness.CleanRightDecoder.input_knownBuckets line 332
  46. theorem OAI.PerfectCompleteness.CleanRightDecoder.input_otherArrays line 338
  47. theorem OAI.PerfectCompleteness.CleanRightDecoder.input_lowerQuotient line 345
  48. abbrev OAI.PerfectCompleteness.CleanRightDecoder.Answer line 354
  49. def OAI.PerfectCompleteness.CleanRightDecoder.kernel line 366
  50. abbrev OAI.PerfectCompleteness.CleanRightDecoder.Seed line 375
  51. def OAI.PerfectCompleteness.CleanRightDecoder.seedLaw line 378
  52. theorem OAI.PerfectCompleteness.CleanRightDecoder.seedLaw_eval line 384
  53. abbrev OAI.PerfectCompleteness.CleanRightDecoder.Form line 395
  54. def OAI.PerfectCompleteness.CleanRightDecoder.forms line 404
  55. def OAI.PerfectCompleteness.CleanRightDecoder.formKernel line 411
  56. theorem OAI.PerfectCompleteness.CleanRightDecoder.seedLaw_forms line 420
  57. abbrev OAI.PerfectCompleteness.CleanDecoderContext.F2 line 456
  58. theorem OAI.PerfectCompleteness.CleanDecoderContext.lowerHeight line 460
  59. structure OAI.PerfectCompleteness.CleanDecoderContext.Exposed line 465
  60. abbrev OAI.PerfectCompleteness.CleanDecoderContext.lower line 491
  61. def OAI.PerfectCompleteness.CleanDecoderContext.path line 494
  62. abbrev OAI.PerfectCompleteness.CleanDecoderContext.CleanChildren line 497
  63. abbrev OAI.PerfectCompleteness.CleanDecoderContext.LeftOwn line 498
  64. abbrev OAI.PerfectCompleteness.CleanDecoderContext.RightOwn line 499
  65. def OAI.PerfectCompleteness.CleanDecoderContext.leftExposed line 501
  66. abbrev OAI.PerfectCompleteness.CleanDecoderContext.leftSlots line 510
  67. abbrev OAI.PerfectCompleteness.CleanDecoderContext.rightSlots line 511
  68. abbrev OAI.PerfectCompleteness.CleanDecoderContext.LeftSeed line 515
  69. abbrev OAI.PerfectCompleteness.CleanDecoderContext.RightSeed line 516
  70. def OAI.PerfectCompleteness.CleanDecoderContext.leftOutput line 521
  71. def OAI.PerfectCompleteness.CleanDecoderContext.leftForm line 524
  72. def OAI.PerfectCompleteness.CleanDecoderContext.rightForm line 527