OAI/Computability/PerfectCompleteness/Machines/NormalizationMachine.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.NormalizationMachine.Tape line 14
  2. abbrev OAI.PerfectCompleteness.NormalizationMachine.Alphabet line 15
  3. abbrev OAI.PerfectCompleteness.NormalizationMachine.State line 16
  4. inductive OAI.PerfectCompleteness.NormalizationMachine.Label line 18
  5. def OAI.PerfectCompleteness.NormalizationMachine.loopTapes line 24
  6. theorem OAI.PerfectCompleteness.NormalizationMachine.loopTapes_injective line 26
  7. def OAI.PerfectCompleteness.NormalizationMachine.program line 31
  8. abbrev OAI.PerfectCompleteness.NormalizationMachine.machine line 43
  9. def OAI.PerfectCompleteness.NormalizationMachine.tapes line 54
  10. def OAI.PerfectCompleteness.NormalizationMachine.cfg line 58
  11. theorem OAI.PerfectCompleteness.NormalizationMachine.initList_eq line 62
  12. theorem OAI.PerfectCompleteness.NormalizationMachine.haltList_eq line 69
  13. theorem OAI.PerfectCompleteness.NormalizationMachine.joinTrace line 76
  14. theorem OAI.PerfectCompleteness.NormalizationMachine.readVariablesTrace line 80
  15. theorem OAI.PerfectCompleteness.NormalizationMachine.readCountTrace line 95
  16. theorem OAI.PerfectCompleteness.NormalizationMachine.headersTrace line 111
  17. theorem OAI.PerfectCompleteness.NormalizationMachine.restoreTrace line 121
  18. theorem OAI.PerfectCompleteness.NormalizationMachine.headerOutputTrace line 140
  19. theorem OAI.PerfectCompleteness.NormalizationMachine.loopTrace line 161
  20. theorem OAI.PerfectCompleteness.NormalizationMachine.formulaBits_eq line 192
  21. def OAI.PerfectCompleteness.NormalizationMachine.steps line 198
  22. theorem OAI.PerfectCompleteness.NormalizationMachine.normalizationTrace line 204
  23. theorem OAI.PerfectCompleteness.NormalizationMachine.header_counts_le line 220
  24. def OAI.PerfectCompleteness.NormalizationMachine.timePolynomial line 227
  25. theorem OAI.PerfectCompleteness.NormalizationMachine.steps_le line 230
  26. def OAI.PerfectCompleteness.NormalizationMachine.outputsInTime line 254
  27. def OAI.PerfectCompleteness.NormalizationMachine.computableInPolyTime line 262
  28. theorem OAI.PerfectCompleteness.NormalizationMachine.machine_finiteAlphabet line 274
  29. theorem OAI.PerfectCompleteness.NormalizationMachine.computation_finiteAlphabet line 278