OAI/Combinatorics/IndependentSets/Machines/FinalCNFStream.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents line 11
  2. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents line 14
  3. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream line 17
  4. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream line 20
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_zero line 25
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_length line 29
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_done line 33
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.remainingEvents_cons line 37
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_zero line 44
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_done line 47
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.processedEvents_succ line 51
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.processed_append_remaining line 58
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_nil line 62
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_cons line 64
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_append line 69
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_nil line 74
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_cons line 77
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_append line 83
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_cons line 89
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_remaining_cons line 96
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_processed_succ line 104
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_split line 113
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_split line 119
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap_rows line 125
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowList_eq_finRange_map line 131
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_all line 137
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.inputStream_remaining_zero line 148
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_accumulator_succ line 152