OAI/Computability/MinUncut/PCP/PreprocessingInternalRows.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.localStep line 14
  2. def OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.destination line 18
  3. def OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.rowIndex line 22
  4. def OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.row line 27
  5. def OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.equalityRelation line 31
  6. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.equalityRelation_apply line 34
  7. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.cloud_rotation line 38
  8. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.source_rotation line 47
  9. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.rotation_internal line 59
  10. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.reverseIndex_internal line 66
  11. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.relation_ext line 76
  12. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.relations_internal line 85
  13. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.row_tail line 92
  14. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.row_reverse line 97
  15. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.row_relation line 104
  16. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.localStep_original line 109
  17. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.localStep_dummy line 114
  18. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.row_tail_original line 118
  19. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.row_tail_dummy line 124
  20. def OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex line 130
  21. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_eq line 135
  22. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_old line 159
  23. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_dummy line 164
  24. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.row_reverse_selectedIndex line 170
  25. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingInternalRows.rowWords_eq line 178