OAI/Computability/PerfectCompleteness/Machines/SourceOccurrenceMachine.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceOccurrenceMachine.Tape line 15
  2. abbrev OAI.PerfectCompleteness.SourceOccurrenceMachine.Alphabet line 16
  3. abbrev OAI.PerfectCompleteness.SourceOccurrenceMachine.State line 17
  4. def OAI.PerfectCompleteness.SourceOccurrenceMachine.clean line 19
  5. inductive OAI.PerfectCompleteness.SourceOccurrenceMachine.Label line 21
  6. def OAI.PerfectCompleteness.SourceOccurrenceMachine.loopTapes line 27
  7. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.loopTapes_injective line 34
  8. def OAI.PerfectCompleteness.SourceOccurrenceMachine.program line 36
  9. abbrev OAI.PerfectCompleteness.SourceOccurrenceMachine.machine line 48
  10. def OAI.PerfectCompleteness.SourceOccurrenceMachine.tapes line 59
  11. def OAI.PerfectCompleteness.SourceOccurrenceMachine.cfg line 63
  12. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.initList_eq line 66
  13. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.haltList_eq line 73
  14. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.joinTrace line 80
  15. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.readVariablesTrace line 84
  16. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.readCountTrace line 102
  17. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.headersTrace line 123
  18. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.restoreTrace line 134
  19. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.headerOutputTrace line 152
  20. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.formulaBits_eq line 172
  21. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.header_counts_le line 178
  22. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.loopTrace line 185
  23. def OAI.PerfectCompleteness.SourceOccurrenceMachine.steps line 216
  24. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.occurrenceTrace line 222
  25. def OAI.PerfectCompleteness.SourceOccurrenceMachine.timePolynomial line 236
  26. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.steps_le line 239
  27. def OAI.PerfectCompleteness.SourceOccurrenceMachine.outputsInTime line 261
  28. def OAI.PerfectCompleteness.SourceOccurrenceMachine.computableInPolyTime line 269
  29. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.machine_finiteAlphabet line 281
  30. theorem OAI.PerfectCompleteness.SourceOccurrenceMachine.computation_finiteAlphabet line 285