OAI/Computability/MinUncut/Estimates/CountedWordParser.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Costed.UnaryWords.finishCounted line 10
  2. def OAI.MinUncut.Costed.UnaryWords.bodyCounted line 11
  3. def OAI.MinUncut.Costed.UnaryWords.finishCountedProgram line 12
  4. def OAI.MinUncut.Costed.UnaryWords.bodyCountedProgram line 13
  5. def OAI.MinUncut.Costed.UnaryWords.parsedCounted line 16
  6. lemma OAI.MinUncut.Costed.UnaryWords.finishCounted_iterate line 17
  7. def OAI.MinUncut.Costed.UnaryWords.parserCountedBound line 22
  8. lemma OAI.MinUncut.Costed.UnaryWords.run_parserCounted line 25
  9. def OAI.MinUncut.Costed.UnaryWords.parserCountedProgram line 49
  10. lemma OAI.MinUncut.Costed.UnaryWords.decodeAux_word line 65
  11. lemma OAI.MinUncut.Costed.UnaryWords.decodeAux_words line 75
  12. lemma OAI.MinUncut.Costed.UnaryWords.parsedCounted_words line 82
  13. def OAI.MinUncut.Costed.Arena.Init.parseWithKey line 92
  14. def OAI.MinUncut.Costed.Arena.Init.parseWithKeyProgram line 93
  15. lemma OAI.MinUncut.Costed.Arena.Init.parseWithKey_spec line 95
  16. lemma OAI.MinUncut.Costed.Arena.Init.exists_initializer line 100
  17. def OAI.MinUncut.Costed.untilBody line 148
  18. def OAI.MinUncut.Costed.untilCode line 152
  19. def OAI.MinUncut.Costed.untilStateBound line 154
  20. def OAI.MinUncut.Costed.untilBound line 155
  21. lemma OAI.MinUncut.Costed.iterate_at_stop line 157
  22. lemma OAI.MinUncut.Costed.run_until line 166
  23. def OAI.MinUncut.Costed.Arena.stoppedTick line 203
  24. def OAI.MinUncut.Costed.Arena.stopExpr line 204
  25. def OAI.MinUncut.Costed.Arena.stopProgram line 205
  26. def OAI.MinUncut.Costed.Arena.stoppedTickProgram line 206
  27. lemma OAI.MinUncut.Costed.Arena.stop_zero line 211
  28. lemma OAI.MinUncut.Costed.Arena.stoppedTick_safe line 214
  29. lemma OAI.MinUncut.Costed.Arena.stoppedTick_encode line 220
  30. lemma OAI.MinUncut.Costed.Arena.stoppedTick_iter_encode line 227
  31. def OAI.MinUncut.Costed.Arena.unboundedControl line 238
  32. lemma OAI.MinUncut.Costed.Arena.unboundedControl_run line 239
  33. def OAI.MinUncut.Costed.Arena.prepareUnbounded line 260
  34. def OAI.MinUncut.Costed.Arena.prepareUnboundedProgram line 262
  35. def OAI.MinUncut.Costed.Arena.unboundedOutput line 264
  36. lemma OAI.MinUncut.Costed.Arena.unboundedOutput_run line 265
  37. def OAI.MinUncut.Costed.Arena.unboundedWordsCode line 277
  38. def OAI.MinUncut.Costed.Arena.unboundedControllerInput line 287
  39. def OAI.MinUncut.Costed.Arena.unboundedControllerState line 288
  40. def OAI.MinUncut.Costed.Arena.unboundedPrepared line 289
  41. def OAI.MinUncut.Costed.Arena.unboundedOutputInput line 290
  42. def OAI.MinUncut.Costed.Arena.unboundedOutputState line 291
  43. def OAI.MinUncut.Costed.Arena.unboundedDropped line 292
  44. def OAI.MinUncut.Costed.Arena.unboundedWordsBound line 293
  45. lemma OAI.MinUncut.Costed.Arena.unboundedWords_run line 298