OAI/Computability/PerfectCompleteness/Machines/NormalizationReadMachine.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.NormalizationReadMachine.Signs line 15
  2. abbrev OAI.PerfectCompleteness.NormalizationReadMachine.Counters line 16
  3. abbrev OAI.PerfectCompleteness.NormalizationReadMachine.State line 17
  4. abbrev OAI.PerfectCompleteness.NormalizationReadMachine.Alphabet line 18
  5. def OAI.PerfectCompleteness.NormalizationReadMachine.clean line 20
  6. def OAI.PerfectCompleteness.NormalizationReadMachine.clauseSigns line 22
  7. def OAI.PerfectCompleteness.NormalizationReadMachine.clauseCounters line 24
  8. inductive OAI.PerfectCompleteness.NormalizationReadMachine.Label line 27
  9. def OAI.PerfectCompleteness.NormalizationReadMachine.afterSign line 36
  10. theorem OAI.PerfectCompleteness.NormalizationReadMachine.afterSign_zero line 40
  11. theorem OAI.PerfectCompleteness.NormalizationReadMachine.afterSign_one line 43
  12. theorem OAI.PerfectCompleteness.NormalizationReadMachine.afterSign_two line 46
  13. def OAI.PerfectCompleteness.NormalizationReadMachine.saveSign line 49
  14. def OAI.PerfectCompleteness.NormalizationReadMachine.rejectSign line 54
  15. def OAI.PerfectCompleteness.NormalizationReadMachine.signInstruction line 58
  16. def OAI.PerfectCompleteness.NormalizationReadMachine.instruction line 69
  17. def OAI.PerfectCompleteness.NormalizationReadMachine.tapes line 75
  18. theorem OAI.PerfectCompleteness.NormalizationReadMachine.tapes_input line 80
  19. theorem OAI.PerfectCompleteness.NormalizationReadMachine.tapes_counter line 86
  20. theorem OAI.PerfectCompleteness.NormalizationReadMachine.tapes_other line 92
  21. theorem OAI.PerfectCompleteness.NormalizationReadMachine.update_input line 97
  22. theorem OAI.PerfectCompleteness.NormalizationReadMachine.update_counter line 108
  23. theorem OAI.PerfectCompleteness.NormalizationReadMachine.fieldTapes_eq line 125
  24. theorem OAI.PerfectCompleteness.NormalizationReadMachine.fieldTrace line 142
  25. theorem OAI.PerfectCompleteness.NormalizationReadMachine.signStep line 161
  26. theorem OAI.PerfectCompleteness.NormalizationReadMachine.joinTrace line 175
  27. theorem OAI.PerfectCompleteness.NormalizationReadMachine.literalTrace line 179
  28. theorem OAI.PerfectCompleteness.NormalizationReadMachine.clauseTrace line 203
  29. def OAI.PerfectCompleteness.NormalizationReadMachine.clauseInTime line 251
  30. theorem OAI.PerfectCompleteness.NormalizationReadMachine.steps_le_encoded_length line 266
  31. abbrev OAI.PerfectCompleteness.NormalizationReadMachine.ConcreteLabel line 273
  32. def OAI.PerfectCompleteness.NormalizationReadMachine.concreteProgram line 275
  33. abbrev OAI.PerfectCompleteness.NormalizationReadMachine.machine line 279
  34. def OAI.PerfectCompleteness.NormalizationReadMachine.machineInTime line 290
  35. theorem OAI.PerfectCompleteness.NormalizationReadMachine.machine_finiteAlphabet line 300