OAI/Computability/RationalHitting/LiftComputation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalHitting.StackLanguage.Runtime.signed line 9
  2. def OAI.RationalHitting.StackLanguage.Runtime.liftTerm line 12
  3. def OAI.RationalHitting.StackLanguage.Runtime.lift line 18
  4. def OAI.RationalHitting.StackLanguage.Runtime.entry line 23
  5. abbrev OAI.RationalHitting.StackLanguage.Runtime.LiftArgs line 26
  6. abbrev OAI.RationalHitting.StackLanguage.Runtime.LiftTermArgs line 27
  7. theorem OAI.RationalHitting.StackLanguage.Runtime.signed_poly line 29
  8. theorem OAI.RationalHitting.StackLanguage.Runtime.liftTerm_poly line 37
  9. theorem OAI.RationalHitting.StackLanguage.Runtime.lift_poly line 60
  10. abbrev OAI.RationalHitting.StackLanguage.Runtime.EntryArgs line 68
  11. theorem OAI.RationalHitting.StackLanguage.Runtime.entry_poly line 69
  12. lemma OAI.RationalHitting.StackLanguage.range_sum_zmod_val line 82
  13. lemma OAI.RationalHitting.StackLanguage.Runtime.signed_eq line 90
  14. lemma OAI.RationalHitting.StackLanguage.Runtime.integerTest_apply line 94
  15. lemma OAI.RationalHitting.StackLanguage.Runtime.liftTerm_eq line 100
  16. lemma OAI.RationalHitting.StackLanguage.Runtime.lift_eq line 113
  17. lemma OAI.RationalHitting.StackLanguage.Runtime.entry_eq line 130