OAI/Computability/MinUncut/Machines/GraphCoreMachine.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Uniform.initializer_exists line 16
  2. def OAI.MinUncut.Uniform.initializerCode line 26
  3. def OAI.MinUncut.Uniform.initializerTime line 27
  4. def OAI.MinUncut.Uniform.initializer_outputs line 28
  5. def OAI.MinUncut.Uniform.coreMachine line 41
  6. lemma OAI.MinUncut.Uniform.core_finite line 43
  7. def OAI.MinUncut.Uniform.coreTime line 46
  8. def OAI.MinUncut.Uniform.core_outputs line 49
  9. abbrev OAI.MinUncut.Costed.Framed.Tape line 66
  10. abbrev OAI.MinUncut.Costed.Framed.Alphabet line 67
  11. abbrev OAI.MinUncut.Costed.Framed.Label line 68
  12. abbrev OAI.MinUncut.Costed.Framed.State line 69
  13. def OAI.MinUncut.Costed.Framed.extra line 71
  14. def OAI.MinUncut.Costed.Framed.program line 85
  15. def OAI.MinUncut.Costed.Framed.machine line 87
  16. lemma OAI.MinUncut.Costed.Framed.finiteAlphabet line 101
  17. def OAI.MinUncut.Costed.Framed.readTapes line 107
  18. def OAI.MinUncut.Costed.Framed.readCfg line 109
  19. def OAI.MinUncut.Costed.Framed.embedded line 111
  20. lemma OAI.MinUncut.Costed.Framed.read_input line 113
  21. lemma OAI.MinUncut.Costed.Framed.read_extra line 115
  22. lemma OAI.MinUncut.Costed.Framed.read_put_input line 116
  23. lemma OAI.MinUncut.Costed.Framed.read_put_extra line 125
  24. lemma OAI.MinUncut.Costed.Framed.read_step line 131
  25. lemma OAI.MinUncut.Costed.Framed.payload_step line 148
  26. lemma OAI.MinUncut.Costed.Framed.read_frames line 163
  27. lemma OAI.MinUncut.Costed.Framed.read_init line 175
  28. lemma OAI.MinUncut.Costed.Framed.finish_step line 185
  29. lemma OAI.MinUncut.Costed.Framed.finish_empty line 200
  30. lemma OAI.MinUncut.Costed.Framed.finish_steps line 217
  31. def OAI.MinUncut.Costed.Framed.execute line 227