OAI/Computability/PerfectCompleteness/Machines/UnaryBlockCopyMachine.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.UnaryBlockCopyMachine.Alphabet line 17
  2. abbrev OAI.PerfectCompleteness.UnaryBlockCopyMachine.State line 18
  3. def OAI.PerfectCompleteness.UnaryBlockCopyMachine.blockWords line 20
  4. def OAI.PerfectCompleteness.UnaryBlockCopyMachine.listValues line 23
  5. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.blockWords_listValues line 26
  6. def OAI.PerfectCompleteness.UnaryBlockCopyMachine.nextField line 39
  7. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.nextField_zero line 42
  8. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.nextField_one line 44
  9. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.nextField_two line 46
  10. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.nextField_three line 48
  11. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.nextField_four line 50
  12. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.nextField_five line 52
  13. def OAI.PerfectCompleteness.UnaryBlockCopyMachine.finish line 55
  14. def OAI.PerfectCompleteness.UnaryBlockCopyMachine.instruction line 58
  15. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.update_source line 67
  16. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.update_destination line 80
  17. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.step_true line 95
  18. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.step_false line 106
  19. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.step_empty line 118
  20. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.fieldTrace line 127
  21. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.joinTrace line 151
  22. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.blockTrace line 155
  23. def OAI.PerfectCompleteness.UnaryBlockCopyMachine.blockInTime line 198
  24. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.listTrace line 210
  25. def OAI.PerfectCompleteness.UnaryBlockCopyMachine.listInTime line 221
  26. abbrev OAI.PerfectCompleteness.UnaryBlockCopyMachine.ConcreteLabel line 236
  27. def OAI.PerfectCompleteness.UnaryBlockCopyMachine.concreteProgram line 238
  28. abbrev OAI.PerfectCompleteness.UnaryBlockCopyMachine.machine line 243
  29. def OAI.PerfectCompleteness.UnaryBlockCopyMachine.machineInTime line 254
  30. theorem OAI.PerfectCompleteness.UnaryBlockCopyMachine.machine_finiteAlphabet line 264