OAI/Combinatorics/IndependentSets/Machines/MachinePaddedExpanderFamilyProgram.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree line 14
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable line 15
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.Tape line 16
  4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.Alphabet line 17
  5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.Label line 18
  6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.State line 19
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyTape line 21
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView line 23
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_left line 27
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_right line 30
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingTape line 39
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView line 43
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_left line 49
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_right line 53
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel line 65
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingLabel line 66
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.main line 67
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry line 68
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates line 70
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates_apply line 74
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.familySource line 80
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingSource line 87
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.program line 92
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.program_family line 99
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.program_ceiling line 105
  26. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialState line 110
  27. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalState line 113
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes line 117
  29. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedCeilingTapes line 121
  30. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes line 125
  31. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes line 130
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes_input line 135
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_input line 138
  34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_power line 141