OAI/Combinatorics/IndependentSets/Machines/MachineExpanderFamilyProgram.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape line 14
  2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 18) line 18
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.Tape line 22
  4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.Alphabet line 23
  5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet line 25
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.alphabet_eq line 27
  7. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.alphabetFintype line 33
  8. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase line 37
  9. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 41) line 41
  10. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel line 45
  11. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 49) line 49
  12. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.OuterLabel line 53
  13. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.Label line 61
  14. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.State line 62
  15. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.RegisterAmbient line 63
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.registerStates line 66
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.registerStates_apply line 73
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.registerStates_symm_apply line 77
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.caller line 80
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.initialState line 83
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.normalizeState line 87
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding line 91
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding_eq_family line 93
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.tableTape line 96
  25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.inputVertexTape line 97
  26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.vertexCountTape line 98
  27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.resultTape line 99
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affineSource line 101
  29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affineDestination line 105
  30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affineCoefficient line 109
  31. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affineExit line 113
  32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.affineStatement line 117
  33. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.drainStatement line 135
  34. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.boolOuterStatement line 143
  35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.outerStatement line 172
  36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.tableReturn line 176
  37. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.program line 178
  38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.program_table line 183
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.program_outer line 190
  40. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.boolView line 194
  41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.boolView_outer line 198
  42. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.tableExecution line 207
  43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.tableExecution_steps line 219
  44. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.tableFrame line 228
  45. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.extraFrame line 234
  46. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes line 239
  47. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.initialTapes line 243
  48. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.familyTapes line 250