OAI/Combinatorics/IndependentSets/Machines/PoweringMachineInitialize.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.ExtraTape line 12
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.GlobalTape line 13
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.Label line 14
  4. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.finalOutput line 16
  5. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement line 18
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_injective line 21
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_start line 27
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_table line 31
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_scratch line 36
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_rowOutput line 41
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_finalOutput line 46
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_header line 51
  13. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement line 57
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_injective line 61
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_rowOutput line 76
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_eq_common line 80
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_data line 84
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_header line 92
  19. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.castTapes line 100
  20. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.castStatement line 103
  21. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.castConfiguration line 106
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_apply line 109
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.castConfiguration_mk line 115
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.stepAux_cast line 121
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.boolAlphabet_eq line 129
  26. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.mergeTapes line 135
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_embedding line 140
  28. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.dropUnit line 148
  29. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.headerStatement line 154
  30. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration line 161
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration_eq line 166
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.stepAux_headerStatement line 180
  33. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.program line 193
  34. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.headerStep line 206
  35. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.headerTrace line 222
  36. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes line 233
  37. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.copyFirstTrace line 236
  38. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.initializeTrace line 267
  39. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.initializeInTime line 279
  40. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.instruction line 292
  41. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.initializeAtInTime line 296
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.final_counter line 311
  43. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.final_vertices line 316
  44. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.final_darts line 319
  45. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineInitialize.final_extra line 322