OAI/Combinatorics/IndependentSets/Machines/MachinePaddedExpanderFamilyFrames.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingInput line 12
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingOutput line 15
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedFrame line 20
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_tapes line 24
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_tapes line 34
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_tapes line 50
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_tapes line 58
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_configuration line 66
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_configuration line 75
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_configuration line 84
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_configuration line 96
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level line 110
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level_shadow line 117
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_level_shadow line 120
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_remainingLevel line 123
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_currentSize line 130
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_table line 137