OAI/Computability/DepthThree/LanguageBitLoopInvariants.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.xorScan line 9
  2. theorem OAI.DepthThreeLowerBound.xorScan_nil line 13
  3. theorem OAI.DepthThreeLowerBound.xorScan_step line 15
  4. theorem OAI.DepthThreeLowerBound.xorScan_eq line 18
  5. theorem OAI.DepthThreeLowerBound.xorBits_append line 25
  6. theorem OAI.DepthThreeLowerBound.xorScan_prefix_invariant line 32
  7. theorem OAI.DepthThreeLowerBound.ofFn_nat_eq_map_range line 36
  8. def OAI.DepthThreeLowerBound.convolutionRow line 43
  9. def OAI.DepthThreeLowerBound.convolutionRows line 47
  10. def OAI.DepthThreeLowerBound.convolutionBit line 50
  11. theorem OAI.DepthThreeLowerBound.convolutionRow_scan line 53
  12. theorem OAI.DepthThreeLowerBound.convolutionRows_scan line 57
  13. theorem OAI.DepthThreeLowerBound.convolutionBit_eq_wordConvolve line 61
  14. def OAI.DepthThreeLowerBound.convolveBitLists line 68
  15. theorem OAI.DepthThreeLowerBound.convolveBitLists_length line 71
  16. theorem OAI.DepthThreeLowerBound.convolveBitLists_eq line 75
  17. theorem OAI.DepthThreeLowerBound.hornerBitLists_nil line 84
  18. theorem OAI.DepthThreeLowerBound.hornerBitLists_cons line 87