OAI/Computability/MinUncut/Estimates/ExpressionOutput.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Preprocess.Syntax.O line 13
  2. lemma OAI.MinUncut.Preprocess.Syntax.O.fixed line 15
  3. lemma OAI.MinUncut.Preprocess.Syntax.O.const line 16
  4. lemma OAI.MinUncut.Preprocess.Syntax.O.reg line 17
  5. lemma OAI.MinUncut.Preprocess.Syntax.O.add line 18
  6. lemma OAI.MinUncut.Preprocess.Syntax.O.sub line 20
  7. lemma OAI.MinUncut.Preprocess.Syntax.O.mul line 22
  8. lemma OAI.MinUncut.Preprocess.Syntax.O.div line 24
  9. lemma OAI.MinUncut.Preprocess.Syntax.O.mod line 26
  10. lemma OAI.MinUncut.Preprocess.Syntax.O.cond line 28
  11. lemma OAI.MinUncut.Preprocess.Syntax.O.eq line 32
  12. lemma OAI.MinUncut.Preprocess.Syntax.O.le line 35
  13. lemma OAI.MinUncut.Preprocess.Syntax.O.at line 38
  14. lemma OAI.MinUncut.Preprocess.Syntax.O.choose line 42
  15. def OAI.MinUncut.Preprocess.Syntax.powCode line 54
  16. lemma OAI.MinUncut.Preprocess.Syntax.c_powCode line 55
  17. lemma OAI.MinUncut.Preprocess.Syntax.O.pow line 59
  18. lemma OAI.MinUncut.Preprocess.Syntax.O.sum line 62
  19. lemma OAI.MinUncut.Preprocess.Syntax.O.first line 65
  20. lemma OAI.MinUncut.Preprocess.Syntax.O.second line 67
  21. lemma OAI.MinUncut.Preprocess.Syntax.O.comp line 69
  22. lemma OAI.MinUncut.Preprocess.Syntax.O.fromC line 71
  23. lemma OAI.MinUncut.Preprocess.Syntax.O.toC line 72
  24. structure OAI.MinUncut.SourceTemplate.Signature line 84
  25. def OAI.MinUncut.SourceTemplate.positiveAt line 88
  26. def OAI.MinUncut.SourceTemplate.signature line 93
  27. def OAI.MinUncut.SourceTemplate.Signature.satisfies line 97
  28. def OAI.MinUncut.SourceTemplate.Signature.valid line 102
  29. def OAI.MinUncut.SourceTemplate.Signature.slot line 106
  30. def OAI.MinUncut.SourceTemplate.Signature.project line 110
  31. lemma OAI.MinUncut.SourceTemplate.signature_valid line 113
  32. lemma OAI.MinUncut.SourceTemplate.signature_project line 120
  33. abbrev OAI.MinUncut.SourceTemplate.LocalKey line 128
  34. def OAI.MinUncut.SourceTemplate.keyAddress line 130
  35. def OAI.MinUncut.SourceTemplate.emptyLocal line 136
  36. def OAI.MinUncut.SourceTemplate.foldedLocal line 140
  37. def OAI.MinUncut.SourceTemplate.localEquation line 146
  38. def OAI.MinUncut.SourceTemplate.Signature.equation line 154
  39. lemma OAI.MinUncut.SourceTemplate.mapEquation_comp line 158
  40. lemma OAI.MinUncut.SourceTemplate.localEquation_spec line 163
  41. lemma OAI.MinUncut.SourceTemplate.signature_equation line 183