OAI/Computability/DepthThree/LanguageBitEvaluator.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.mul_remainder_modByMonic line 13
  2. theorem OAI.DepthThreeLowerBound.wordPoly_mod_self line 26
  3. def OAI.DepthThreeLowerBound.wordHorner line 32
  4. theorem OAI.DepthThreeLowerBound.wordPoly_horner line 38
  5. def OAI.DepthThreeLowerBound.wordHash line 61
  6. theorem OAI.DepthThreeLowerBound.wordHash_eq line 65
  7. def OAI.DepthThreeLowerBound.multiplyBitLists line 72
  8. theorem OAI.DepthThreeLowerBound.multiplyBitLists_length line 75
  9. theorem OAI.DepthThreeLowerBound.multiplyBitLists_correct line 79
  10. def OAI.DepthThreeLowerBound.hornerBitLists line 85
  11. theorem OAI.DepthThreeLowerBound.hornerBitLists_length line 89
  12. theorem OAI.DepthThreeLowerBound.hornerBitLists_correct line 93
  13. def OAI.DepthThreeLowerBound.ParsedInput.evaluationBits line 101
  14. theorem OAI.DepthThreeLowerBound.ParsedInput.wordPoly_evaluationBits line 105
  15. def OAI.DepthThreeLowerBound.ParsedInput.evaluateBits line 110
  16. theorem OAI.DepthThreeLowerBound.ParsedInput.evaluateBits_eq line 113
  17. def OAI.DepthThreeLowerBound.languageBits line 125
  18. theorem OAI.DepthThreeLowerBound.languageBits_eq_language line 130