OAI/Computability/PerfectCompleteness/Machines/CompletedEdgeMachine.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.CompletedEdgeMachine.key line 26
  2. def OAI.PerfectCompleteness.CompletedEdgeMachine.edge line 30
  3. def OAI.PerfectCompleteness.CompletedEdgeMachine.edgeBits line 37
  4. theorem OAI.PerfectCompleteness.CompletedEdgeMachine.edgeBits_eq line 41
  5. def OAI.PerfectCompleteness.CompletedEdgeMachine.leftMap line 51
  6. def OAI.PerfectCompleteness.CompletedEdgeMachine.rightMap line 53
  7. theorem OAI.PerfectCompleteness.CompletedEdgeMachine.leftMap_injective line 55
  8. theorem OAI.PerfectCompleteness.CompletedEdgeMachine.rightMap_injective line 56
  9. theorem OAI.PerfectCompleteness.CompletedEdgeMachine.forward_ne_left line 58
  10. theorem OAI.PerfectCompleteness.CompletedEdgeMachine.forward_ne_right line 59
  11. theorem OAI.PerfectCompleteness.CompletedEdgeMachine.leftMap_work line 61
  12. theorem OAI.PerfectCompleteness.CompletedEdgeMachine.rightMap_work line 64
  13. abbrev OAI.PerfectCompleteness.CompletedEdgeMachine.Alphabet line 69
  14. abbrev OAI.PerfectCompleteness.CompletedEdgeMachine.State line 70
  15. abbrev OAI.PerfectCompleteness.CompletedEdgeMachine.clean line 71
  16. def OAI.PerfectCompleteness.CompletedEdgeMachine.leftTapes line 73
  17. def OAI.PerfectCompleteness.CompletedEdgeMachine.rightTapes line 74
  18. inductive OAI.PerfectCompleteness.CompletedEdgeMachine.Label line 76
  19. def OAI.PerfectCompleteness.CompletedEdgeMachine.main line 82
  20. def OAI.PerfectCompleteness.CompletedEdgeMachine.instruction line 86
  21. def OAI.PerfectCompleteness.CompletedEdgeMachine.finalTapes line 103
  22. def OAI.PerfectCompleteness.CompletedEdgeMachine.budget line 114
  23. def OAI.PerfectCompleteness.CompletedEdgeMachine.edgeInTime line 120
  24. theorem OAI.PerfectCompleteness.CompletedEdgeMachine.finalTapes_frame line 219
  25. theorem OAI.PerfectCompleteness.CompletedEdgeMachine.label_finite line 227
  26. theorem OAI.PerfectCompleteness.CompletedEdgeMachine.state_finite line 229
  27. theorem OAI.PerfectCompleteness.CompletedEdgeMachine.workAlphabet_finite line 231