OAI/Combinatorics/IndependentSets/Machines/OwnerData.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerData line 13
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerSeedStep line 21
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.copyOwnerTrace line 39
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerPlacement line 53
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerInitialData_eq line 65
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerBodyTrace line 68
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerGuardStep line 84
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerGuardExit line 98
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerIncrementStep line 109
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerPrefix line 129
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed line 132
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerPrefixTrace line 139
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerLoopTrace line 169
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.ownerStageTrace line 181
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.owner_output_eq_ownerPrefix line 191
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.cleaned line 207
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime line 212
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.drainTrace line 217
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.cleanupPrefixTrace line 225
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTrace line 239
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.finalStacks line 245
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.cleaned_finalStacks line 248
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.cleaned_length_le line 268
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_le line 282
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_final_le line 298
  26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.headerOutput line 362
  27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.oldOutput line 365
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.finalOutput line 368
  29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.totalTime line 371
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.old_output_eq_originalPrefix line 377
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Top.finalOutput_eq line 382