OAI/Combinatorics/IndependentSets/Machines/MachineExpanderFamilyAffine.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_scratch line 11
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affine_source_ne_destination line 14
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affine_scratch_ne_destination line 17
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes line 20
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_other line 27
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_source line 33
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_scratch line 38
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affineResultTapes_destination line 43
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseBoolTrace line 51
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseTrace line 96
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affinePhaseInTime line 111
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.copyCountInTime line 124
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.multiplySizeInTime line 141