OAI/Combinatorics/IndependentSets/Machines/AmbientRelation.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.State line 16
2. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.readRelationAt line 18
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.stepAux_readRelationAt line 23
4. inductive OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.Tape line 44
5. instance OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.(instance at line 49) line 49
6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.Ambient line 54
7. abbrev OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.Plan line 55
8. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.values line 57
9. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan line 60
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_length line 64
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_bits line 67
12. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.source line 75
13. inductive OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.Label line 78
14. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.guard line 92
15. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.program line 99
16. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.machine line 146
17. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles line 157
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headRoles_injective line 161
19. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headPhaseInTime line 164
20. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.workingTapes line 180
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.workingTapes_operands line 193
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_input line 200
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_tail line 207
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_head line 214
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_accumulator line 221
26. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.update_working_rowIndex line 228
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.source_ne_scratch line 236
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.source_ne_accumulator line 239