OAI/Computability/MinUncut/Estimates/UniformEquationOutput.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Preprocess.UEncoding.out_elimSum line 12
  2. lemma OAI.MinUncut.Preprocess.UEncoding.map_eqTuple line 37
  3. lemma OAI.MinUncut.Preprocess.UEncoding.map_eqFirst line 39
  4. lemma OAI.MinUncut.Preprocess.UEncoding.map_eqSecond line 42
  5. lemma OAI.MinUncut.Preprocess.UEncoding.map_eqThird line 46
  6. lemma OAI.MinUncut.Preprocess.UEncoding.map_eqRhs line 51
  7. lemma OAI.MinUncut.Preprocess.Source.out_keyTag line 59
  8. lemma OAI.MinUncut.Preprocess.Source.out_keyTable line 66
  9. def OAI.MinUncut.SourceTemplate.sourceExpressions line 82
  10. lemma OAI.MinUncut.SourceTemplate.sourceExpressions_eval line 86
  11. lemma OAI.MinUncut.SourceTemplate.emitted_source line 93
  12. def OAI.MinUncut.SourceTemplate.sourceVariableExpr line 112
  13. def OAI.MinUncut.SourceTemplate.sourceCountExpr line 115
  14. def OAI.MinUncut.SourceTemplate.sourceStageWords line 117
  15. def OAI.MinUncut.SourceTemplate.sourceStageProgram line 121
  16. lemma OAI.MinUncut.SourceTemplate.sourceVariableExpr_eval line 125
  17. lemma OAI.MinUncut.SourceTemplate.sourceCountExpr_eval line 130
  18. lemma OAI.MinUncut.SourceTemplate.sourceStageWords_spec line 143
  19. lemma OAI.MinUncut.Preprocess.Syntax.O.sourceAddress line 165
  20. abbrev OAI.MinUncut.Preprocess.Syntax.sourceArgs line 184
  21. lemma OAI.MinUncut.Preprocess.Syntax.map_sourceContext line 185
  22. lemma OAI.MinUncut.Preprocess.Syntax.out_sourceEquationExpressions line 188
  23. lemma OAI.MinUncut.Preprocess.Syntax.c_sourceExpressions line 201
  24. lemma OAI.MinUncut.Preprocess.Syntax.c_sourceVariableExpr line 210
  25. lemma OAI.MinUncut.Preprocess.Syntax.c_sourceCountExpr line 215
  26. lemma OAI.MinUncut.Preprocess.Syntax.c_sourceStageCode line 219
  27. lemma OAI.MinUncut.Costed.SourceWords.sum_flatMap_nat line 238
  28. lemma OAI.MinUncut.Costed.SourceWords.tupleList_sum line 244
  29. lemma OAI.MinUncut.Costed.SourceWords.tupleDemands_failure line 249
  30. lemma OAI.MinUncut.Costed.SourceWords.generatedDemands_failure line 260
  31. lemma OAI.MinUncut.Costed.SourceWords.generated_failure_eq line 272