OAI/Computability/BinPacking/Computation/MachineExpanderFamilyBoundary.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.caller_initialState line 12
  2. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.caller_normalizeState line 15
  3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_initialState line 18
  4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_update_level line 22
  5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.initialTapes_initialize line 34
  6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.actualStep_of_boolStep line 51
  7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.bool_initializeStep line 64
  8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_succStep line 77
  9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_zeroStep line 90
  10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.bool_doneStep line 102
  11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.initializeStep line 110
  12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_succStep line 122
  13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_zeroStep line 135
  14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.doneStep line 145
  15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.initialize_boundaryStep line 153
  16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_succStep line 169
  17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_zeroStep line 180