OAI/NumberTheory/SingleFold/TuringSimulation.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SingleFold.TM2Macro.Symbol line 12
  2. abbrev OAI.SingleFold.TM2Macro.Store line 13
  3. abbrev OAI.SingleFold.TM2Macro.Stack line 14
  4. instance OAI.SingleFold.TM2Macro.(instance at line 15) line 15
  5. abbrev OAI.SingleFold.TM2Macro.Stmt line 18
  6. abbrev OAI.SingleFold.TM2Macro.Reg line 19
  7. inductive OAI.SingleFold.TM2Macro.Label line 20
  8. def OAI.SingleFold.TM2Macro.digit line 30
  9. def OAI.SingleFold.TM2Macro.symbol line 32
  10. lemma OAI.SingleFold.TM2Macro.symbol_zero line 34
  11. lemma OAI.SingleFold.TM2Macro.symbol_digit line 35
  12. lemma OAI.SingleFold.TM2Macro.digit_pos line 36
  13. def OAI.SingleFold.TM2Macro.pack line 38
  14. lemma OAI.SingleFold.TM2Macro.pack_nil line 41
  15. lemma OAI.SingleFold.TM2Macro.pack_cons line 42
  16. lemma OAI.SingleFold.TM2Macro.pack_div line 43
  17. lemma OAI.SingleFold.TM2Macro.pack_mod line 47
  18. lemma OAI.SingleFold.TM2Macro.pack_symbol line 51
  19. lemma OAI.SingleFold.TM2Macro.pack_restore line 53
  20. def OAI.SingleFold.TM2Macro.program line 60
  21. def OAI.SingleFold.TM2Macro.values line 78
  22. def OAI.SingleFold.TM2Macro.encode line 79
  23. def OAI.SingleFold.TM2Macro.codeCfg line 81
  24. lemma OAI.SingleFold.TM2Macro.values_inl line 83
  25. lemma OAI.SingleFold.TM2Macro.values_inr line 84
  26. lemma OAI.SingleFold.TM2Macro.values_update line 85
  27. lemma OAI.SingleFold.TM2Macro.stepAux_reaches line 92
  28. lemma OAI.SingleFold.TM2Macro.respects line 144
  29. lemma OAI.SingleFold.TM2Macro.eval_dom line 151
  30. lemma OAI.SingleFold.TM2Macro.trNat_posNum line 158
  31. lemma OAI.SingleFold.TM2Macro.trNat_div line 160
  32. def OAI.SingleFold.TM2Macro.initValues line 182
  33. def OAI.SingleFold.TM2Macro.initCfg line 183
  34. lemma OAI.SingleFold.TM2Macro.initValues_main line 185
  35. lemma OAI.SingleFold.TM2Macro.initValues_rev line 186
  36. lemma OAI.SingleFold.TM2Macro.initValues_input line 187
  37. lemma OAI.SingleFold.TM2Macro.initValues_update_main line 188
  38. lemma OAI.SingleFold.TM2Macro.initValues_update_rev line 194
  39. lemma OAI.SingleFold.TM2Macro.initValues_update_input line 200
  40. lemma OAI.SingleFold.TM2Macro.prepend line 206
  41. lemma OAI.SingleFold.TM2Macro.reverse_loop line 209
  42. lemma OAI.SingleFold.TM2Macro.divide_loop line 229
  43. lemma OAI.SingleFold.TM2Macro.one_input line 254
  44. def OAI.SingleFold.TM2Macro.inputPrefix line 271
  45. def OAI.SingleFold.TM2Macro.clearPrefix line 273
  46. lemma OAI.SingleFold.TM2Macro.prefix_succ line 274
  47. lemma OAI.SingleFold.TM2Macro.prefix_update line 279
  48. lemma OAI.SingleFold.TM2Macro.clearPrefix_update line 284
  49. lemma OAI.SingleFold.TM2Macro.trList_append line 294
  50. lemma OAI.SingleFold.TM2Macro.init_loop line 300
  51. lemma OAI.SingleFold.TM2Macro.initialize_reaches line 317
  52. def OAI.SingleFold.Macro.Instr.map line 334
  53. def OAI.SingleFold.Macro.Instr.Within line 338
  54. def OAI.SingleFold.Macro.Cfg.map line 341
  55. def OAI.SingleFold.Macro.retract line 342
  56. def OAI.SingleFold.Macro.restrict line 344
  57. lemma OAI.SingleFold.Macro.retract_val line 346
  58. lemma OAI.SingleFold.Macro.instr_retract line 349
  59. lemma OAI.SingleFold.Macro.cfg_next_map line 352
  60. lemma OAI.SingleFold.Macro.restrict_next line 357
  61. lemma OAI.SingleFold.Macro.restrict_respects line 364
  62. lemma OAI.SingleFold.Macro.restrict_eval_dom line 375