OAI/Combinatorics/IndependentSets/Machines/Copy.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsCut.CounterMachine.Data.ext line 13
  2. theorem OAI.IndependentSetsCut.CounterMachine.Command.Within.loop line 19
  3. theorem OAI.IndependentSetsCut.CounterMachine.Command.Within.inc line 31
  4. theorem OAI.IndependentSetsCut.CounterMachine.Command.Within.dec line 33
  5. theorem OAI.IndependentSetsCut.CounterMachine.Command.Within.skip line 35
  6. theorem OAI.IndependentSetsCut.CounterMachine.Command.Within.clear line 37
  7. theorem OAI.IndependentSetsCut.CounterMachine.Command.Within.move line 40
  8. def OAI.IndependentSetsCut.CounterMachine.Command.copy line 44
  9. theorem OAI.IndependentSetsCut.CounterMachine.Command.copy_evaluates line 47
  10. def OAI.IndependentSetsCut.CounterMachine.Command.mulAdd line 78
  11. theorem OAI.IndependentSetsCut.CounterMachine.Command.mulAdd_evaluates line 81
  12. def OAI.IndependentSetsCut.CounterMachine.Command.put line 118
  13. theorem OAI.IndependentSetsCut.CounterMachine.Command.put_evaluates line 122
  14. def OAI.IndependentSetsCut.CounterMachine.Command.subFrom line 133
  15. theorem OAI.IndependentSetsCut.CounterMachine.Command.subFrom_evaluates line 135
  16. theorem OAI.IndependentSetsCut.CounterMachine.Command.rewind_evaluates line 151
  17. def OAI.IndependentSetsCut.CounterMachine.Command.skipInput line 169
  18. theorem OAI.IndependentSetsCut.CounterMachine.Command.skipInput_evaluates line 171
  19. def OAI.IndependentSetsCut.CounterMachine.Command.inputBit line 202
  20. theorem OAI.IndependentSetsCut.CounterMachine.Command.inputBit_evaluates line 205