OAI/Combinatorics/IndependentSets/Machines/Restrict.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsCut.CounterMachine.Data.restrict line 9
  2. def OAI.IndependentSetsCut.CounterMachine.Command.Bounded line 14
  3. def OAI.IndependentSetsCut.CounterMachine.Command.regCount line 22
  4. theorem OAI.IndependentSetsCut.CounterMachine.Command.bounded_of_count line 30
  5. def OAI.IndependentSetsCut.CounterMachine.Command.restrict line 33
  6. theorem OAI.IndependentSetsCut.CounterMachine.Command.restrict_inc line 45
  7. theorem OAI.IndependentSetsCut.CounterMachine.Command.restrict_dec line 57
  8. theorem OAI.IndependentSetsCut.CounterMachine.Command.Evaluates.restrict line 69
  9. def OAI.IndependentSetsCut.CounterMachine.Command.finite line 90
  10. theorem OAI.IndependentSetsCut.CounterMachine.Command.finite_evaluates line 93
  11. def OAI.IndependentSetsCut.CounterMachine.table line 102
  12. def OAI.IndependentSetsCut.CounterMachine.emit line 106
  13. theorem OAI.IndependentSetsCut.CounterMachine.emit_evaluates line 108
  14. def OAI.IndependentSetsCut.CounterMachine.print line 120
  15. theorem OAI.IndependentSetsCut.CounterMachine.print_evaluates line 124
  16. def OAI.IndependentSetsCut.CounterMachine.eraseInput line 195
  17. theorem OAI.IndependentSetsCut.CounterMachine.eraseInput_evaluates line 197