OAI/NumberTheory/SingleFold/RecursiveEnumeration.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleFold.TM2Macro.Good line 11
  2. inductive OAI.SingleFold.TM2Macro.BLabel line 15
  3. def OAI.SingleFold.TM2Macro.forget line 25
  4. lemma OAI.SingleFold.TM2Macro.forget_good line 29
  5. lemma OAI.SingleFold.TM2Macro.forget_surj line 32
  6. instance OAI.SingleFold.TM2Macro.finite_good line 44
  7. lemma OAI.SingleFold.TM2Macro.program_within line 48
  8. def OAI.SingleFold.TM2Macro.statements line 75
  9. lemma OAI.SingleFold.TM2Macro.statements_self line 76
  10. lemma OAI.SingleFold.TM2Macro.statements_sub line 78
  11. lemma OAI.SingleFold.TM2Macro.statements_goto line 83
  12. instance OAI.SingleFold.TM2Macro.fintype_good line 89
  13. abbrev OAI.SingleFold.TM2Macro.FiniteState line 90
  14. def OAI.SingleFold.TM2Macro.finStart line 91
  15. def OAI.SingleFold.TM2Macro.finProgram line 92
  16. def OAI.SingleFold.TM2Macro.counterProgram line 94
  17. def OAI.SingleFold.TM2Macro.inputSlot line 96
  18. def OAI.SingleFold.TM2Macro.counterInput line 98
  19. lemma OAI.SingleFold.TM2Macro.counterInput_eq line 99
  20. lemma OAI.SingleFold.TM2Macro.counter_halts line 105
  21. lemma OAI.SingleFold.TM2Macro.exists_code line 128
  22. theorem OAI.SingleFold.TM2Macro.exists_counter line 143