OAI/Computability/PerfectCompleteness/Machines/SourceTupleMachine.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceTupleMachine.Signs line 14
  2. abbrev OAI.PerfectCompleteness.SourceTupleMachine.Shape line 15
  3. abbrev OAI.PerfectCompleteness.SourceTupleMachine.Alphabet line 16
  4. abbrev OAI.PerfectCompleteness.SourceTupleMachine.State line 17
  5. structure OAI.PerfectCompleteness.SourceTupleMachine.Data line 19
  6. def OAI.PerfectCompleteness.SourceTupleMachine.state line 24
  7. def OAI.PerfectCompleteness.SourceTupleMachine.initial line 27
  8. def OAI.PerfectCompleteness.SourceTupleMachine.update line 30
  9. def OAI.PerfectCompleteness.SourceTupleMachine.result line 38
  10. def OAI.PerfectCompleteness.SourceTupleMachine.cost line 43
  11. def OAI.PerfectCompleteness.SourceTupleMachine.steps line 47
  12. theorem OAI.PerfectCompleteness.SourceTupleMachine.result_prepared line 51
  13. theorem OAI.PerfectCompleteness.SourceTupleMachine.result_shapes line 65
  14. theorem OAI.PerfectCompleteness.SourceTupleMachine.result_finRange_prepared line 81
  15. theorem OAI.PerfectCompleteness.SourceTupleMachine.result_finRange_shapes line 87
  16. theorem OAI.PerfectCompleteness.SourceTupleMachine.cost_le line 95
  17. theorem OAI.PerfectCompleteness.SourceTupleMachine.steps_le line 107
  18. abbrev OAI.PerfectCompleteness.SourceTupleMachine.LocalLabel line 122
  19. abbrev OAI.PerfectCompleteness.SourceTupleMachine.Label line 123
  20. def OAI.PerfectCompleteness.SourceTupleMachine.localMain line 126
  21. def OAI.PerfectCompleteness.SourceTupleMachine.save line 129
  22. def OAI.PerfectCompleteness.SourceTupleMachine.localInstruction line 135
  23. def OAI.PerfectCompleteness.SourceTupleMachine.instruction line 140
  24. def OAI.PerfectCompleteness.SourceTupleMachine.entry line 146
  25. theorem OAI.PerfectCompleteness.SourceTupleMachine.sequenceTrace line 149
  26. theorem OAI.PerfectCompleteness.SourceTupleMachine.tupleTrace line 200
  27. def OAI.PerfectCompleteness.SourceTupleMachine.tupleInTime line 220
  28. theorem OAI.PerfectCompleteness.SourceTupleMachine.finiteState line 243
  29. theorem OAI.PerfectCompleteness.SourceTupleMachine.finiteLabels line 245