OAI/Computability/PerfectCompleteness/Machines/FixedUnaryRepresentationMachine.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.Mode line 14
  2. abbrev OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.Mode.enumList line 18
  3. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.Mode.enumList_getElem?_ctorIdx_eq line 20
  4. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.Mode.enumList_nodup line 24
  5. instance OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.(instance at line 26) line 26
  6. inductive OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.Tape line 30
  7. abbrev OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.Alphabet line 36
  8. abbrev OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.State line 37
  9. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.sourceWord line 39
  10. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.targetWord line 43
  11. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.cost line 47
  12. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.cost_le line 51
  13. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.LocalLabel line 54
  14. instance OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.(instance at line 58) line 58
  15. instance OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.(instance at line 63) line 63
  16. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.localMain line 68
  17. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.localTape line 74
  18. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.localTape_injective line 79
  19. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.«stacks» line 84
  20. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.update_destination line 90
  21. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.update line 104
  22. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.result line 108
  23. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.steps line 112
  24. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.sequence_steps line 115
  25. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.result_apply line 125
  26. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.result_finRange line 142
  27. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.steps_le line 149
  28. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.localInstruction line 164
  29. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.localTrace line 172
  30. abbrev OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.Label line 206
  31. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.entry line 209
  32. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.instruction line 214
  33. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.sequenceTrace line 219
  34. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.familyTrace line 239
  35. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.familyInTime line 253
  36. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.cleanupTapes line 271
  37. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.cleanupTapes_length line 274
  38. abbrev OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.CleanupLabel line 277
  39. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.cleanupEntry line 279
  40. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.cleanupInstruction line 282
  41. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.cleanup_finalTapes line 286
  42. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.cleanup_lengthSum line 293
  43. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.cleanupTrace line 299
  44. def OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.cleanupInTime line 312
  45. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.finiteState line 326
  46. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.finiteLabels line 328
  47. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationMachine.finiteAlphabet line 330