OAI/Computability/PerfectCompleteness/Decoding/FixedStoppedNativeProjection.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.leftSlots_sourceSampleEquiv line 28
  2. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.rightSlots_sourceSampleEquiv line 38
  3. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.projection_sourceSampleEquiv_heq line 48
  4. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.fillProjection_outsidePresentation_heq line 61
  5. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.fullProjection_sources_heq line 82
  6. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.projection_function_heq line 96
  7. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.projectedSlots_physicalRead_eq line 107
  8. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.projectedSlots_tag_eq_rightSlots line 126
  9. abbrev OAI.PerfectCompleteness.FixedStoppedNativeProjection.physicalSample line 141
  10. abbrev OAI.PerfectCompleteness.FixedStoppedNativeProjection.innerTag line 144
  11. abbrev OAI.PerfectCompleteness.FixedStoppedNativeProjection.originalQuestions line 151
  12. abbrev OAI.PerfectCompleteness.FixedStoppedNativeProjection.path line 154
  13. abbrev OAI.PerfectCompleteness.FixedStoppedNativeProjection.childSample line 157
  14. abbrev OAI.PerfectCompleteness.FixedStoppedNativeProjection.sources line 160
  15. abbrev OAI.PerfectCompleteness.FixedStoppedNativeProjection.flags line 165
  16. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.physicalSources_eq line 170
  17. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.flags_eq line 196
  18. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.outside_eq line 199
  19. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.fill_outside_eq line 216
  20. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.leftSlots_eq line 229
  21. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.physicalRightSlots_eq line 249
  22. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.rightSlots_eq line 276
  23. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.projection_apply_heq line 291
  24. theorem OAI.PerfectCompleteness.FixedStoppedNativeProjection.projection_heq line 331