OAI/Combinatorics/IndependentSets/Machines/FinalCNFMachine.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Buffer line 11
2. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.readUnarySlots line 17
3. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.unaryBits line 28
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.unaryBits_eq_encodeWords line 31
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.unaryBits_length_le line 38
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.statementPushBound_readUnarySlots line 48
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.stepAux_readUnarySlots line 59
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.stepAux_readUnaryAll line 83
9. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.unaryBlockMapAt line 96
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.stepAux_unaryBlockMapAt line 104
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.step_unaryBlockMapAt line 119
12. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.unaryBlockInTime line 132
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.unaryBits_relation line 149
14. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.readerStateEquiv line 160