OAI/Computability/PerfectCompleteness/Foundations/SourceTuplePlacement.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceTuplePlacement.Tape line 15
  2. abbrev OAI.PerfectCompleteness.SourceTuplePlacement.Label line 16
  3. abbrev OAI.PerfectCompleteness.SourceTuplePlacement.State line 17
  4. abbrev OAI.PerfectCompleteness.SourceTuplePlacement.Shape line 18
  5. abbrev OAI.PerfectCompleteness.SourceTuplePlacement.Signs line 19
  6. abbrev OAI.PerfectCompleteness.SourceTuplePlacement.Alphabet line 20
  7. def OAI.PerfectCompleteness.SourceTuplePlacement.nativeProgram line 24
  8. def OAI.PerfectCompleteness.SourceTuplePlacement.instruction line 28
  9. def OAI.PerfectCompleteness.SourceTuplePlacement.entry line 32
  10. def OAI.PerfectCompleteness.SourceTuplePlacement.tapes line 36
  11. theorem OAI.PerfectCompleteness.SourceTuplePlacement.tape_injective line 41
  12. theorem OAI.PerfectCompleteness.SourceTuplePlacement.tapes_placed line 47
  13. theorem OAI.PerfectCompleteness.SourceTuplePlacement.tapes_complement line 55
  14. theorem OAI.PerfectCompleteness.SourceTuplePlacement.tapes_eq_base line 61
  15. theorem OAI.PerfectCompleteness.SourceTuplePlacement.complement_preserved line 75
  16. theorem OAI.PerfectCompleteness.SourceTuplePlacement.tupleTrace line 84
  17. def OAI.PerfectCompleteness.SourceTuplePlacement.tupleInTime line 110
  18. theorem OAI.PerfectCompleteness.SourceTuplePlacement.finiteState line 138
  19. theorem OAI.PerfectCompleteness.SourceTuplePlacement.finiteLabels line 140
  20. theorem OAI.PerfectCompleteness.SourceTuplePlacement.finiteAlphabet line 143