OAI/Combinatorics/IndependentSets/Machines/FinalCNFLoop.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.LoopInvariant line 12
2. structure OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.LoopRun line 23
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowInvariant_succ line 35
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowWords_nonempty line 55
5. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.loopInTime line 59
6. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.emittedBytes line 118
7. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rawBudget line 122
8. structure OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.RawRun line 127
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.header_loopInvariant line 135
10. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rawRun line 150