OAI/Combinatorics/IndependentSets/Expansion/PoweringGlobalConfiguration.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_injective line 10
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_output line 13
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.output_ne_placement line 19
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_placement line 23
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_placement line 29
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerVertices line 35
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerDarts line 39
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_headerDarts line 43
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_output line 46
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_output line 49
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_scratch line 52
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_scratch line 57
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.scratch_ne_output line 62
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.boolList_mpr_eq line 67
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.haltList_tapes line 70
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalConfiguration.haltList_eq line 79