OAI/Computability/DepthThree/LanguageBitHornerLoop.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.hornerStep line 9
  2. theorem OAI.DepthThreeLowerBound.hornerStep_length line 12
  3. theorem OAI.DepthThreeLowerBound.hornerStep_eq_word line 16
  4. def OAI.DepthThreeLowerBound.hornerFrom line 30
  5. theorem OAI.DepthThreeLowerBound.hornerFrom_nil line 34
  6. theorem OAI.DepthThreeLowerBound.hornerFrom_cons line 37
  7. theorem OAI.DepthThreeLowerBound.hornerFrom_append line 41
  8. theorem OAI.DepthThreeLowerBound.hornerFrom_append_singleton line 47
  9. theorem OAI.DepthThreeLowerBound.hornerFrom_length line 53
  10. theorem OAI.DepthThreeLowerBound.hornerFrom_zero_eq_hornerBitLists line 63
  11. theorem OAI.DepthThreeLowerBound.block_flatten_length line 79