OAI/Computability/PerfectCompleteness/Machines/SourceOccurrenceIndexMachine.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.Alphabet line 18
  2. abbrev OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.State line 19
  3. def OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.clean line 21
  4. inductive OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.Label line 23
  5. abbrev OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.Label.enumList line 30

    Source documentation

    A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.)

    protected abbrev Label.enumList : List Label := [.copyOut, .copyBack, .delimiter]

    Mentions: OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.Label

  6. theorem OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.Label.enumList_getElem?_ctorIdx_eq line 32
  7. theorem OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.Label.enumList_nodup line 36
  8. instance OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.(instance at line 38) line 38
  9. def OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.main line 42
  10. def OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.instruction line 44
  11. def OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.steps line 52
  12. theorem OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.joinTrace line 54
  13. theorem OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.indexTrace line 58
  14. def OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.indexInTime line 87
  15. theorem OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.label_finite line 104
  16. theorem OAI.PerfectCompleteness.SourceOccurrenceIndexMachine.state_finite line 106