OAI/Combinatorics/IndependentSets/Machines/Command.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.IndependentSetsCut.CounterMachine.Command line 9
  2. def OAI.IndependentSetsCut.CounterMachine.Command.Label line 23
  3. instance OAI.IndependentSetsCut.CounterMachine.Command.labelFintype line 30
  4. def OAI.IndependentSetsCut.CounterMachine.Command.entry line 38
  5. def OAI.IndependentSetsCut.CounterMachine.Command.code line 43
  6. def OAI.IndependentSetsCut.CounterMachine.Command.incData line 71
  7. def OAI.IndependentSetsCut.CounterMachine.Command.decData line 73
  8. def OAI.IndependentSetsCut.CounterMachine.Command.readData line 75
  9. def OAI.IndependentSetsCut.CounterMachine.Command.backData line 77
  10. def OAI.IndependentSetsCut.CounterMachine.Command.discardData line 79
  11. def OAI.IndependentSetsCut.CounterMachine.Command.writeData line 80
  12. inductive OAI.IndependentSetsCut.CounterMachine.Command.Evaluates line 82
  13. def OAI.IndependentSetsCut.CounterMachine.advance line 110
  14. def OAI.IndependentSetsCut.CounterMachine.atCfg line 113
  15. def OAI.IndependentSetsCut.CounterMachine.Runs line 115
  16. theorem OAI.IndependentSetsCut.CounterMachine.runs_one line 118
  17. theorem OAI.IndependentSetsCut.CounterMachine.Runs.trans line 122
  18. theorem OAI.IndependentSetsCut.CounterMachine.Command.trace line 128