OAI/Combinatorics/IndependentSets/Expansion/PoweringInitializeFrame.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra line 12
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_table line 17
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_other line 21
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_scratch line 26
  5. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.preparedTapes line 31
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.prepared_commonRole line 37
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.prepared_ready line 45
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.prepared_start line 55
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.prepared_counter line 62
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.prepared_output line 69
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.prepared_vertices line 74
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.prepared_darts line 77
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.prepared_source line 81
  14. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.preparedCfg line 84
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.initialGlobalTapes_eq line 89
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.machine_initialStacks line 104
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.initList_eq line 108
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.tableBits_head line 117
  19. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringInitializeFrame.initializeInTime line 121