OAI/Computability/MinUncut/Estimates/ExpressionEffectivity.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Preprocess.Syntax.p_dropCode line 10
  2. lemma OAI.MinUncut.Preprocess.Syntax.p_constCode line 14
  3. lemma OAI.MinUncut.Preprocess.Syntax.p_atCode line 18
  4. def OAI.MinUncut.Preprocess.Syntax.bin line 20
  5. def OAI.MinUncut.Preprocess.Syntax.branch line 21
  6. lemma OAI.MinUncut.Preprocess.Syntax.p_bin line 22
  7. lemma OAI.MinUncut.Preprocess.Syntax.p_branch line 24
  8. def OAI.MinUncut.Preprocess.Syntax.C line 29
  9. lemma OAI.MinUncut.Preprocess.Syntax.C.fixed line 32
  10. lemma OAI.MinUncut.Preprocess.Syntax.C.const line 33
  11. lemma OAI.MinUncut.Preprocess.Syntax.C.reg line 34
  12. lemma OAI.MinUncut.Preprocess.Syntax.C.add line 35
  13. lemma OAI.MinUncut.Preprocess.Syntax.C.sub line 37
  14. lemma OAI.MinUncut.Preprocess.Syntax.C.mul line 39
  15. lemma OAI.MinUncut.Preprocess.Syntax.C.div line 41
  16. lemma OAI.MinUncut.Preprocess.Syntax.C.mod line 43
  17. lemma OAI.MinUncut.Preprocess.Syntax.cond_code line 45
  18. lemma OAI.MinUncut.Preprocess.Syntax.C.cond line 47
  19. lemma OAI.MinUncut.Preprocess.Syntax.eqOf_code line 51
  20. lemma OAI.MinUncut.Preprocess.Syntax.eq_code line 55
  21. lemma OAI.MinUncut.Preprocess.Syntax.le_code line 60
  22. lemma OAI.MinUncut.Preprocess.Syntax.at_code line 63
  23. lemma OAI.MinUncut.Preprocess.Syntax.C.eq line 65
  24. lemma OAI.MinUncut.Preprocess.Syntax.C.le line 72
  25. lemma OAI.MinUncut.Preprocess.Syntax.C.at line 77
  26. lemma OAI.MinUncut.Preprocess.Syntax.powCode_eq line 81
  27. lemma OAI.MinUncut.Preprocess.Syntax.C.pow line 89
  28. def OAI.MinUncut.Preprocess.Syntax.sumCode line 95
  29. lemma OAI.MinUncut.Preprocess.Syntax.p_sumCode line 96
  30. lemma OAI.MinUncut.Preprocess.Syntax.sumCode_eq line 98
  31. lemma OAI.MinUncut.Preprocess.Syntax.C.sum line 102