OAI/Combinatorics/IndependentSets/Machines/MachineExpanderRowDivision.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.controlStatement_inverse line 11
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.transportedDivision line 18
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.divisionStates_apply line 77
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.divisionState line 81
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.divisionOutput line 86
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.firstDivisionTrace line 92
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.secondDivisionTrace line 133
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_source line 177
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_quotient line 189
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_remainder line 198
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_other line 205
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.firstDivisionInTime line 215
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.secondDivisionInTime line 239