OAI/Computability/RationalHitting/Feasibility.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RationalHitting.StackLanguage.Feasible.id line 11
  2. theorem OAI.RationalHitting.StackLanguage.Feasible.const line 12
  3. theorem OAI.RationalHitting.StackLanguage.Feasible.comp line 14
  4. theorem OAI.RationalHitting.StackLanguage.Feasible.pair line 16
  5. theorem OAI.RationalHitting.StackLanguage.Feasible.fst line 19
  6. theorem OAI.RationalHitting.StackLanguage.Feasible.snd line 21
  7. theorem OAI.RationalHitting.StackLanguage.Feasible.prodMap line 23
  8. theorem OAI.RationalHitting.StackLanguage.Feasible.recode line 26
  9. theorem OAI.RationalHitting.StackLanguage.Feasible.of_eq line 30
  10. theorem OAI.RationalHitting.StackLanguage.Feasible.branch line 34
  11. theorem OAI.RationalHitting.StackLanguage.Feasible.cond line 37
  12. theorem OAI.RationalHitting.StackLanguage.Feasible.iterate line 42
  13. theorem OAI.RationalHitting.StackLanguage.Feasible.appendWord line 48
  14. theorem OAI.RationalHitting.StackLanguage.Feasible.reverseWord line 50
  15. def OAI.RationalHitting.TimeBound.power line 59
  16. instance OAI.RationalHitting.TimeBound.(instance at line 62) line 62
  17. lemma OAI.RationalHitting.TimeBound.eval_pow line 63
  18. lemma OAI.RationalHitting.StackLanguage.add_bits_length line 75
  19. lemma OAI.RationalHitting.StackLanguage.eval_normalize_single line 81
  20. def OAI.RationalHitting.StackLanguage.addClean line 95
  21. lemma OAI.RationalHitting.StackLanguage.eval_addClean line 96
  22. def OAI.RationalHitting.StackLanguage.Procedure.binaryAdd line 115
  23. def OAI.RationalHitting.StackLanguage.Procedure.binaryMul line 123
  24. theorem OAI.RationalHitting.StackLanguage.Feasible.binaryAdd line 148
  25. theorem OAI.RationalHitting.StackLanguage.Feasible.binaryMul line 150
  26. theorem OAI.RationalHitting.StackLanguage.Feasible.unaryAdd line 153