OAI/Computability/PerfectCompleteness/Machines/SignedTupleCleanupMachineLemmas.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SignedTupleCleanupMachine.Tape line 21
  2. abbrev OAI.PerfectCompleteness.SignedTupleCleanupMachine.State line 22
  3. abbrev OAI.PerfectCompleteness.SignedTupleCleanupMachine.Alphabet line 23
  4. def OAI.PerfectCompleteness.SignedTupleCleanupMachine.localTapes line 27
  5. def OAI.PerfectCompleteness.SignedTupleCleanupMachine.chosen line 33
  6. def OAI.PerfectCompleteness.SignedTupleCleanupMachine.selected line 36
  7. theorem OAI.PerfectCompleteness.SignedTupleCleanupMachine.chosen_length line 42
  8. theorem OAI.PerfectCompleteness.SignedTupleCleanupMachine.mem_chosen line 54
  9. theorem OAI.PerfectCompleteness.SignedTupleCleanupMachine.finalTapes_eq line 73
  10. theorem OAI.PerfectCompleteness.SignedTupleCleanupMachine.selected_length_le line 95
  11. def OAI.PerfectCompleteness.SignedTupleCleanupMachine.steps line 130
  12. theorem OAI.PerfectCompleteness.SignedTupleCleanupMachine.steps_le line 134
  13. abbrev OAI.PerfectCompleteness.SignedTupleCleanupMachine.Label line 166
  14. def OAI.PerfectCompleteness.SignedTupleCleanupMachine.instruction line 168
  15. def OAI.PerfectCompleteness.SignedTupleCleanupMachine.entry line 173
  16. theorem OAI.PerfectCompleteness.SignedTupleCleanupMachine.cleanupTrace line 176
  17. def OAI.PerfectCompleteness.SignedTupleCleanupMachine.cleanupInTime line 195
  18. theorem OAI.PerfectCompleteness.SignedTupleCleanupMachine.finiteLabels line 213
  19. abbrev OAI.PerfectCompleteness.SignedTuplePreparationMachine.Tape line 229
  20. abbrev OAI.PerfectCompleteness.SignedTuplePreparationMachine.State line 230
  21. abbrev OAI.PerfectCompleteness.SignedTuplePreparationMachine.Alphabet line 231
  22. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.variableEquiv line 235
  23. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.digitTape line 237
  24. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.digitView line 242
  25. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.digitView_left line 248
  26. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.digitView_right line 252
  27. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.variableTape line 273
  28. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.variableView line 278
  29. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.variableView_left line 284
  30. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.variableView_right line 288
  31. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.variableValues line 310
  32. inductive OAI.PerfectCompleteness.SignedTuplePreparationMachine.Label line 314
  33. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.variableEntry line 320
  34. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.sourceEntry line 323
  35. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.entry line 326
  36. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.instruction line 330
  37. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.digit_initial_eq line 339
  38. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.digit_final_eq line 350
  39. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.source_initial_eq line 372
  40. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.source_final_eq line 384
  41. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.variable_initial_eq line 401
  42. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.variable_final_eq line 411
  43. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.budget line 433
  44. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.budget_le line 437
  45. def OAI.PerfectCompleteness.SignedTuplePreparationMachine.prepareInTime line 444
  46. theorem OAI.PerfectCompleteness.SignedTuplePreparationMachine.finiteLabels line 489
  47. def OAI.PerfectCompleteness.SourceTupleScheduleMachine.shapeSigns line 504
  48. def OAI.PerfectCompleteness.SourceTupleScheduleMachine.signTuple line 508
  49. def OAI.PerfectCompleteness.SourceTupleScheduleMachine.sourceSigns line 513
  50. theorem OAI.PerfectCompleteness.SourceTupleScheduleMachine.signTuple_source line 521
  51. abbrev OAI.PerfectCompleteness.SourceTupleScheduleMachine.State line 532
  52. def OAI.PerfectCompleteness.SourceTupleScheduleMachine.table line 535
  53. def OAI.PerfectCompleteness.SourceTupleScheduleMachine.keys line 539
  54. theorem OAI.PerfectCompleteness.SourceTupleScheduleMachine.mem_keys line 541
  55. abbrev OAI.PerfectCompleteness.SourceTupleScheduleMachine.Alphabet line 547
  56. def OAI.PerfectCompleteness.SourceTupleScheduleMachine.exitAt line 549
  57. def OAI.PerfectCompleteness.SourceTupleScheduleMachine.instruction line 554
  58. def OAI.PerfectCompleteness.SourceTupleScheduleMachine.pushBound line 559
  59. theorem OAI.PerfectCompleteness.SourceTupleScheduleMachine.instruction_pushBound line 564
  60. theorem OAI.PerfectCompleteness.SourceTupleScheduleMachine.scheduleStep line 572
  61. theorem OAI.PerfectCompleteness.SourceTupleScheduleMachine.sourceTrace line 591
  62. def OAI.PerfectCompleteness.SourceTupleScheduleMachine.sourceInTime line 614