OAI/Computability/PerfectCompleteness/Machines/BinaryHeaderMachine.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.BinaryHeaderMachine.Alphabet line 16
  2. abbrev OAI.PerfectCompleteness.BinaryHeaderMachine.State line 17
  3. def OAI.PerfectCompleteness.BinaryHeaderMachine.delimiter line 23
  4. def OAI.PerfectCompleteness.BinaryHeaderMachine.tapes line 27
  5. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.tapes_variables line 32
  6. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.tapes_clauses line 39
  7. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.tapes_destination line 46
  8. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.tapes_other line 52
  9. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.update_variables line 58
  10. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.update_clauses line 75
  11. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.update_destination line 89
  12. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.clauseDelimiterStep line 108
  13. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.variableDelimiterStep line 120
  14. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.clauseCounterTrace line 132
  15. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.variableCounterTrace line 152
  16. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.joinTrace line 171
  17. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.headerTrace line 177
  18. def OAI.PerfectCompleteness.BinaryHeaderMachine.headerInTime line 206
  19. abbrev OAI.PerfectCompleteness.BinaryHeaderMachine.ConcreteTape line 221
  20. abbrev OAI.PerfectCompleteness.BinaryHeaderMachine.ConcreteLabel line 222
  21. def OAI.PerfectCompleteness.BinaryHeaderMachine.concreteProgram line 224
  22. abbrev OAI.PerfectCompleteness.BinaryHeaderMachine.machine line 231
  23. def OAI.PerfectCompleteness.BinaryHeaderMachine.start line 242
  24. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.haltList_eq line 246
  25. def OAI.PerfectCompleteness.BinaryHeaderMachine.machineInTime line 254
  26. theorem OAI.PerfectCompleteness.BinaryHeaderMachine.machine_finiteAlphabet line 264