OAI/Computability/PerfectCompleteness/Machines/SourcePhysicalTapeLaw.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourcePhysicalTapeLaw.Tag line 28
  2. def OAI.PerfectCompleteness.SourcePhysicalTapeLaw.insideSlots line 31
  3. def OAI.PerfectCompleteness.SourcePhysicalTapeLaw.nativeSlots line 35
  4. def OAI.PerfectCompleteness.SourcePhysicalTapeLaw.projectedSlots line 39
  5. def OAI.PerfectCompleteness.SourcePhysicalTapeLaw.fullProjection line 43
  6. abbrev OAI.PerfectCompleteness.SourcePhysicalTapeLaw.Sample line 51
  7. abbrev OAI.PerfectCompleteness.SourcePhysicalTapeLaw.Exterior line 53
  8. abbrev OAI.PerfectCompleteness.SourcePhysicalTapeLaw.Record line 55
  9. def OAI.PerfectCompleteness.SourcePhysicalTapeLaw.rebuild line 58
  10. def OAI.PerfectCompleteness.SourcePhysicalTapeLaw.sourceTag line 67
  11. def OAI.PerfectCompleteness.SourcePhysicalTapeLaw.tag line 71
  12. def OAI.PerfectCompleteness.SourcePhysicalTapeLaw.observe line 76
  13. def OAI.PerfectCompleteness.SourcePhysicalTapeLaw.observeFiber line 86
  14. theorem OAI.PerfectCompleteness.SourcePhysicalTapeLaw.rebuild_law line 96
  15. theorem OAI.PerfectCompleteness.SourcePhysicalTapeLaw.observeFiber_law line 106
  16. def OAI.PerfectCompleteness.SourcePhysicalTapeLaw.law line 128
  17. def OAI.PerfectCompleteness.SourcePhysicalTapeLaw.tagLaw line 135
  18. theorem OAI.PerfectCompleteness.SourcePhysicalTapeLaw.observe_law line 139
  19. theorem OAI.PerfectCompleteness.SourcePhysicalTapeLaw.observe_tape line 191
  20. theorem OAI.PerfectCompleteness.SourcePhysicalTapeLaw.observe_native_arrays line 202
  21. theorem OAI.PerfectCompleteness.SourcePhysicalTapeLaw.observeFiber_native_arrays line 216