OAI/Combinatorics/IndependentSets/Machines/Block.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.encodedBlockStmt line 15
  2. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.encodedBlockAt line 22
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_encodedBlockAt line 26
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockStmt line 35
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockAt line 50
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.step_encodedBlockAt line 61
  7. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.rowAt line 78
  8. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.machine line 83
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.machine_statementPushBound line 94
  10. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRow.machineInTime line 99
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.guardConfiguration line 130
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.bodyConfiguration line 136
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.exitConfiguration line 141
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.BodyTraces line 146
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.totalSteps line 155
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.totalSteps_zero line 158
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.totalSteps_succ line 161
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.loopTrace line 166
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.totalSteps_le line 199
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.loopInTime line 210
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.baseFrame line 231
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.counterFrame line 242
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCountedLoop.loopTrace_framed line 253