OAI/Combinatorics/IndependentSets/Machines/MachineCloudRank.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.update_memory_spare line 12
  2. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.RankLabel line 17
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.rankSkip line 23
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.rankProgram line 26
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.rankProgram_skip line 45
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.rowGuard_succ line 50
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.rowGuard_zero line 61
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.zeroRowsTrace line 69
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.rankRowTrace line 83
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.prefixTime line 119
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.prefixTrace line 123
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.prefixTime_le line 150
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.queryWord line 160
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.encoded_rows_split line 163
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.rankSteps line 171
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.rankTrace line 176
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.rankSteps_le line 234
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.idxOf_filter_prefix line 247
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.tableRows_length line 266
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.cloudRank_eq_prefix_count line 269
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.cloudRankTrace line 282
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudRank.cloudRankInTime line 305