OAI/Computability/MinUncut/Games/PoweringMasterState.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.OtherRegisters line 13
  2. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.Master line 14
  3. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.CompareState line 15
  4. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.RowState line 16
  5. def OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.compareEquiv line 18
  6. def OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.rowEquiv line 21
  7. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.compareEquiv_apply line 27
  8. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.compareEquiv_symm_apply line 31
  9. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.rowEquiv_apply line 35
  10. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.rowEquiv_symm_apply line 39
  11. def OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.withBuffer line 43
  12. def OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.clean line 46
  13. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.equalityBit_clean line 48
  14. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.rowEquiv_withBuffer line 51
  15. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.compareEquiv_withBuffer line 54
  16. def OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.clearBuffer line 57
  17. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.clearBuffer_apply line 60
  18. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.clearBuffer_withBuffer line 65
  19. def OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.encodedBlockAt line 72
  20. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.stepAux_encodedBlockAt line 77
  21. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.step_encodedBlockAt line 90
  22. def OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.rowAt line 102
  23. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.step_rowAt_clean line 107
  24. def OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.rowInTime line 124
  25. def OAI.MinUncutGames.Foundations.Complexity.PoweringMasterState.headerInTime line 146