OAI/Computability/MinUncut/PCP/EquationEmit.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.Label line 15
2. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.Label.enumList line 20
3. theorem OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.Label.enumList_getElem?_ctorIdx_eq line 23
4. theorem OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.Label.enumList_nodup line 27
5. instance OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.(instance at line 29) line 29
6. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.Alphabet line 33
7. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.State line 34
8. def OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.rhsBit line 36
9. def OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.steps line 38
10. def OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.statement line 43
11. def OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.program line 66
12. def OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.prefixTapes line 70
13. theorem OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.prefixTapes_other line 73
14. theorem OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.equationTrace line 77
15. def OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.equationInTime line 148
16. def OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.programInTime line 167
17. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.Tape line 182
18. def OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.machine line 184
19. def OAI.MinUncutGames.Foundations.Hastad.SourceEquationEmit.machineInTime line 195