OAI/Computability/PerfectCompleteness/Machines/SignedDescriptorStageMachine.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SignedDescriptorStageMachine.Descriptor line 22
  2. abbrev OAI.PerfectCompleteness.SignedDescriptorStageMachine.Context line 24
  3. abbrev OAI.PerfectCompleteness.SignedDescriptorStageMachine.State line 26
  4. def OAI.PerfectCompleteness.SignedDescriptorStageMachine.clean line 29
  5. def OAI.PerfectCompleteness.SignedDescriptorStageMachine.loaded line 32
  6. def OAI.PerfectCompleteness.SignedDescriptorStageMachine.save line 37
  7. inductive OAI.PerfectCompleteness.SignedDescriptorStageMachine.Label line 41
  8. theorem OAI.PerfectCompleteness.SignedDescriptorStageMachine.state_finite line 48
  9. theorem OAI.PerfectCompleteness.SignedDescriptorStageMachine.label_finite line 51
  10. abbrev OAI.PerfectCompleteness.SignedDescriptorStageMachine.Alphabet line 62
  11. def OAI.PerfectCompleteness.SignedDescriptorStageMachine.selected line 64
  12. def OAI.PerfectCompleteness.SignedDescriptorStageMachine.finish line 71
  13. theorem OAI.PerfectCompleteness.SignedDescriptorStageMachine.finish_trace line 77
  14. theorem OAI.PerfectCompleteness.SignedDescriptorStageMachine.finish_pushBound line 85
  15. def OAI.PerfectCompleteness.SignedDescriptorStageMachine.instruction line 92
  16. def OAI.PerfectCompleteness.SignedDescriptorStageMachine.finalTapes line 106
  17. theorem OAI.PerfectCompleteness.SignedDescriptorStageMachine.finalTapes_frame line 114
  18. theorem OAI.PerfectCompleteness.SignedDescriptorStageMachine.finalTapes_count line 125
  19. theorem OAI.PerfectCompleteness.SignedDescriptorStageMachine.stageBudget line 136
  20. def OAI.PerfectCompleteness.SignedDescriptorStageMachine.stageInTimeForDescriptor line 139
  21. def OAI.PerfectCompleteness.SignedDescriptorStageMachine.stageInTime line 230