OAI/Combinatorics/IndependentSets/Machines/FinalLabel.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsCut.CounterMachine.advance_simulation line 12
  2. theorem OAI.IndependentSetsCut.CounterMachine.iterate_simulation line 18
  3. abbrev OAI.IndependentSetsCut.CounterMachine.Command.FinalLabel line 29
  4. def OAI.IndependentSetsCut.CounterMachine.Command.finalCode line 31
  5. def OAI.IndependentSetsCut.CounterMachine.Command.initial line 35
  6. def OAI.IndependentSetsCut.CounterMachine.Command.finiteMachine line 38
  7. theorem OAI.IndependentSetsCut.CounterMachine.Command.finiteMachine_initial line 41
  8. def OAI.IndependentSetsCut.CounterMachine.Command.machine_run line 49
  9. theorem OAI.IndependentSetsCut.CounterMachine.Command.finiteMachine_finite_alphabet line 66
  10. def OAI.IndependentSetsCut.CounterMachine.Data.set line 77
  11. theorem OAI.IndependentSetsCut.CounterMachine.Data.set_self line 80
  12. theorem OAI.IndependentSetsCut.CounterMachine.Data.set_set line 83
  13. theorem OAI.IndependentSetsCut.CounterMachine.Data.set_reg_same line 86
  14. theorem OAI.IndependentSetsCut.CounterMachine.Data.set_reg_ne line 89
  15. theorem OAI.IndependentSetsCut.CounterMachine.Data.set_comm line 92
  16. def OAI.IndependentSetsCut.CounterMachine.Command.clear line 102
  17. def OAI.IndependentSetsCut.CounterMachine.Command.move line 104
  18. theorem OAI.IndependentSetsCut.CounterMachine.Command.clear_evaluates line 106
  19. theorem OAI.IndependentSetsCut.CounterMachine.Command.move_evaluates line 122
  20. def OAI.IndependentSetsCut.CounterMachine.Command.Within line 150
  21. theorem OAI.IndependentSetsCut.CounterMachine.Command.Within.seq line 153
  22. theorem OAI.IndependentSetsCut.CounterMachine.Command.Within.mono line 159