OAI/Computability/PerfectCompleteness/Machines/TupleEnumerationMachine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.TupleEnumerationMachine.Tape line 13
  2. inductive OAI.PerfectCompleteness.TupleEnumerationMachine.Label line 15
  3. abbrev OAI.PerfectCompleteness.TupleEnumerationMachine.Alphabet line 24
  4. abbrev OAI.PerfectCompleteness.TupleEnumerationMachine.Register line 25
  5. abbrev OAI.PerfectCompleteness.TupleEnumerationMachine.Configuration line 26
  6. def OAI.PerfectCompleteness.TupleEnumerationMachine.checkAt line 29
  7. def OAI.PerfectCompleteness.TupleEnumerationMachine.currentAt line 32
  8. def OAI.PerfectCompleteness.TupleEnumerationMachine.remainingAt line 35
  9. def OAI.PerfectCompleteness.TupleEnumerationMachine.body line 38
  10. def OAI.PerfectCompleteness.TupleEnumerationMachine.program line 40
  11. def OAI.PerfectCompleteness.TupleEnumerationMachine.resetAt line 47
  12. def OAI.PerfectCompleteness.TupleEnumerationMachine.tapes line 50
  13. def OAI.PerfectCompleteness.TupleEnumerationMachine.configuration line 58
  14. def OAI.PerfectCompleteness.TupleEnumerationMachine.setDigit line 63
  15. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.setDigit_self line 66
  16. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.setDigit_zero line 69
  17. def OAI.PerfectCompleteness.TupleEnumerationMachine.prependBlocks line 76
  18. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.prependBlocks_eq line 80
  19. def OAI.PerfectCompleteness.TupleEnumerationMachine.outputBlock line 86
  20. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.outputBlock_zero line 91
  21. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.outputBlock_succ line 94
  22. def OAI.PerfectCompleteness.TupleEnumerationMachine.fillDigits line 99
  23. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.fillDigits_snoc line 103
  24. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.range_eq_ofFn line 116
  25. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.outputBlock_eq_tupleOrder line 123
  26. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.fillDigits_all line 151
  27. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.outputBlock_all line 156
  28. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.tapes_output line 163
  29. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.tapes_digit line 174
  30. def OAI.PerfectCompleteness.TupleEnumerationMachine.leafInTime line 217
  31. def OAI.PerfectCompleteness.TupleEnumerationMachine.leafBound line 235
  32. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.leafBudget_le line 237
  33. theorem OAI.PerfectCompleteness.TupleEnumerationMachine.existsTree line 247
  34. def OAI.PerfectCompleteness.TupleEnumerationMachine.enumerateInTime line 389
  35. def OAI.PerfectCompleteness.TupleEnumerationMachine.machine line 406