OAI/Combinatorics/IndependentSets/Machines/TableIterationFiniteAlphabet.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.Complexity.TableIterationFiniteAlphabet.initial line 11
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.TableIterationFiniteAlphabet.finalCNF line 16
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.TableIterationFiniteAlphabet.counter line 21
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.TableIterationFiniteAlphabet.counted line 33
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.TableIterationFiniteAlphabet.iteration line 36
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.TableIterationFiniteAlphabet.table line 40
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.TableIterationFiniteAlphabet.gapMap line 44
  8. inductive OAI.IndependentSetsCut.CounterMachine.Tape line 53
  9. inductive OAI.IndependentSetsCut.CounterMachine.Instruction line 57
  10. structure OAI.IndependentSetsCut.CounterMachine.Data line 68
  11. structure OAI.IndependentSetsCut.CounterMachine.Configuration line 74
  12. def OAI.IndependentSetsCut.CounterMachine.Instruction.execute line 79
  13. def OAI.IndependentSetsCut.CounterMachine.step line 97
  14. def OAI.IndependentSetsCut.CounterMachine.tapes line 100
  15. def OAI.IndependentSetsCut.CounterMachine.embed line 106
  16. def OAI.IndependentSetsCut.CounterMachine.goto line 109
  17. def OAI.IndependentSetsCut.CounterMachine.Instruction.code line 112
  18. theorem OAI.IndependentSetsCut.CounterMachine.tapes_inc line 130
  19. theorem OAI.IndependentSetsCut.CounterMachine.tapes_dec line 140
  20. theorem OAI.IndependentSetsCut.CounterMachine.tapes_read line 150
  21. theorem OAI.IndependentSetsCut.CounterMachine.tapes_back line 156
  22. theorem OAI.IndependentSetsCut.CounterMachine.tapes_write line 162
  23. theorem OAI.IndependentSetsCut.CounterMachine.instruction_simulation line 167
  24. theorem OAI.IndependentSetsCut.CounterMachine.step_simulation line 209
  25. def OAI.IndependentSetsCut.CounterMachine.machine line 217
  26. theorem OAI.IndependentSetsCut.CounterMachine.finite_tape_alphabet line 228