OAI/Computability/PerfectCompleteness/Machines/TargetHeaderMachine.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PerfectCompleteness.TargetHeaderMachine.Alphabet line 17
2. abbrev OAI.PerfectCompleteness.TargetHeaderMachine.State line 18
3. inductive OAI.PerfectCompleteness.TargetHeaderMachine.Label line 20
4. abbrev OAI.PerfectCompleteness.TargetHeaderMachine.Label.enumList line 26

   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 := [.copyLast, .restoreLast, .pushAlphabet,
   …

   Mentions: OAI.PerfectCompleteness.TargetHeaderMachine.Label

5. theorem OAI.PerfectCompleteness.TargetHeaderMachine.Label.enumList_getElem?_ctorIdx_eq line 29
6. theorem OAI.PerfectCompleteness.TargetHeaderMachine.Label.enumList_nodup line 33
7. instance OAI.PerfectCompleteness.TargetHeaderMachine.(instance at line 35) line 35
8. def OAI.PerfectCompleteness.TargetHeaderMachine.main line 39
9. def OAI.PerfectCompleteness.TargetHeaderMachine.instruction line 43
10. theorem OAI.PerfectCompleteness.TargetHeaderMachine.instruction_pushBound line 61
11. theorem OAI.PerfectCompleteness.TargetHeaderMachine.pushAlphabetStep line 68
12. theorem OAI.PerfectCompleteness.TargetHeaderMachine.joinTrace line 80
13. theorem OAI.PerfectCompleteness.TargetHeaderMachine.headerTrace line 84
14. def OAI.PerfectCompleteness.TargetHeaderMachine.headerInTime line 135
15. def OAI.PerfectCompleteness.TargetHeaderMachine.increment line 151
16. theorem OAI.PerfectCompleteness.TargetHeaderMachine.encodeWord_zero line 154
17. theorem OAI.PerfectCompleteness.TargetHeaderMachine.incrementStep line 156
18. def OAI.PerfectCompleteness.TargetHeaderMachine.incrementInTime line 168
19. theorem OAI.PerfectCompleteness.TargetHeaderMachine.finiteState line 178
20. theorem OAI.PerfectCompleteness.TargetHeaderMachine.finiteAlphabet line 181