OAI/Computability/MinUncut/PCP/PreprocessingLazyWords.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.row line 14
  2. def OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.trueRelation line 18
  3. def OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.stayRow line 20
  4. def OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.moveRow line 23
  5. def OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.reverseMap line 29
  6. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.relation_ext line 31
  7. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.row_lazy_stay line 38
  8. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.row_lazy_move line 51
  9. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.stayRow_reverse_val line 64
  10. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.moveRow_reverse_val line 69
  11. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.relationWords_true line 77
  12. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.stayRow_words line 81
  13. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.moveRow_words line 87
  14. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.ofFn_rowIndex line 94
  15. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.flatRows_list line 108
  16. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.ofFn_lazyPorts line 115
  17. def OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.vertexRows line 128
  18. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.vertexRows_length line 132
  19. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.flatRows_lazy line 137
  20. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.vertexRows_words line 147
  21. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.tableWords_lazy line 167
  22. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingLazyWords.tableBits_lazy line 172