OAI/Computability/MinUncut/Estimates/TemplateExpressions.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.SourceTemplate.functionExpr line 17
  2. lemma OAI.MinUncut.SourceTemplate.functionExpr_eval line 20
  3. def OAI.MinUncut.SourceTemplate.positiveExpr line 26
  4. def OAI.MinUncut.SourceTemplate.sameExpr line 28
  5. def OAI.MinUncut.SourceTemplate.signatureExpr line 31
  6. lemma OAI.MinUncut.SourceTemplate.positiveExpr_eval line 34
  7. lemma OAI.MinUncut.SourceTemplate.sameExpr_eval line 45
  8. lemma OAI.MinUncut.SourceTemplate.signatureExpr_eval line 59
  9. def OAI.MinUncut.SourceTemplate.signatureLookup line 64
  10. lemma OAI.MinUncut.SourceTemplate.signatureLookup_eval line 67
  11. def OAI.MinUncut.SourceTemplate.sampledExpr line 73
  12. lemma OAI.MinUncut.SourceTemplate.sampledExpr_eval line 76
  13. def OAI.MinUncut.SourceTemplate.addressExpr line 83
  14. lemma OAI.MinUncut.SourceTemplate.addressExpr_eval line 93
  15. def OAI.MinUncut.SourceTemplate.equationExpressions line 106
  16. lemma OAI.MinUncut.SourceTemplate.equationExpressions_eval line 113
  17. lemma OAI.MinUncut.Preprocess.Syntax.O.ofEq line 132
  18. def OAI.MinUncut.Preprocess.Syntax.eqCode line 135
  19. lemma OAI.MinUncut.Preprocess.Syntax.p_eqCode line 137
  20. def OAI.MinUncut.Preprocess.Syntax.lookupCode line 141
  21. lemma OAI.MinUncut.Preprocess.Syntax.p_lookupCode line 143
  22. lemma OAI.MinUncut.Preprocess.Syntax.lookupCode_eq line 150
  23. lemma OAI.MinUncut.Preprocess.Syntax.O.lookup line 159
  24. lemma OAI.MinUncut.Preprocess.Syntax.O.sum_enum line 162
  25. lemma OAI.MinUncut.Preprocess.Syntax.O.sum_fin line 168
  26. lemma OAI.MinUncut.Preprocess.Syntax.out_constantTable line 174
  27. lemma OAI.MinUncut.Preprocess.Syntax.O.functionExpr line 177
  28. def OAI.MinUncut.Preprocess.Source.positions line 195
  29. def OAI.MinUncut.Preprocess.Source.slots line 196
  30. def OAI.MinUncut.Preprocess.Source.answers line 197
  31. def OAI.MinUncut.Preprocess.Source.lefts line 198
  32. def OAI.MinUncut.Preprocess.Source.rights line 199
  33. def OAI.MinUncut.Preprocess.Source.coordinates line 200
  34. def OAI.MinUncut.Preprocess.Source.polarities line 201
  35. def OAI.MinUncut.Preprocess.Source.equalities line 202
  36. def OAI.MinUncut.Preprocess.Source.signatures line 204
  37. lemma OAI.MinUncut.Preprocess.Source.signatures_encoding line 206
  38. lemma OAI.MinUncut.Preprocess.Source.map_positive line 207
  39. lemma OAI.MinUncut.Preprocess.Source.map_same line 210
  40. lemma OAI.MinUncut.Preprocess.Source.map_satisfies line 215
  41. lemma OAI.MinUncut.Preprocess.Source.map_same_at line 223
  42. lemma OAI.MinUncut.Preprocess.Source.map_answer_at line 227
  43. lemma OAI.MinUncut.Preprocess.Source.map_consistent line 233
  44. lemma OAI.MinUncut.Preprocess.Source.map_valid line 244
  45. def OAI.MinUncut.Preprocess.Source.slotContexts line 275
  46. lemma OAI.MinUncut.Preprocess.Source.map_slot line 278
  47. lemma OAI.MinUncut.Preprocess.Source.map_project line 286
  48. lemma OAI.MinUncut.Preprocess.Source.map_anchor line 293
  49. lemma OAI.MinUncut.Preprocess.UEncoding.map_xor line 302
  50. lemma OAI.MinUncut.Preprocess.UEncoding.map_representative line 306
  51. def OAI.MinUncut.SourceTemplate.paddedRep line 324
  52. lemma OAI.MinUncut.SourceTemplate.extend_representative line 327
  53. lemma OAI.MinUncut.SourceTemplate.findValid_map line 337
  54. def OAI.MinUncut.SourceTemplate.rawLocal line 344
  55. lemma OAI.MinUncut.SourceTemplate.rawLocal_eq line 353