OAI/Computability/DepthThree/LanguageBitReductionLoop.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.modulusUpdateLoop line 7
  2. theorem OAI.DepthThreeLowerBound.modulusUpdateLoop_zero line 12
  3. theorem OAI.DepthThreeLowerBound.modulusUpdateLoop_step line 15
  4. theorem OAI.DepthThreeLowerBound.modulusUpdateLoop_length line 19
  5. theorem OAI.DepthThreeLowerBound.modulusUpdateLoop_getD line 26
  6. theorem OAI.DepthThreeLowerBound.modulusUpdateLoop_above line 52
  7. theorem OAI.DepthThreeLowerBound.modulusUpdateLoop_high line 59
  8. def OAI.DepthThreeLowerBound.cancelByUpdates line 65
  9. theorem OAI.DepthThreeLowerBound.cancelByUpdates_length line 69
  10. theorem OAI.DepthThreeLowerBound.cancelByUpdates_getD line 73
  11. def OAI.DepthThreeLowerBound.reduceByUpdates line 95
  12. theorem OAI.DepthThreeLowerBound.reduceByUpdates_zero line 99
  13. theorem OAI.DepthThreeLowerBound.reduceByUpdates_step line 101
  14. theorem OAI.DepthThreeLowerBound.reduceByUpdates_length line 104
  15. theorem OAI.DepthThreeLowerBound.cancelStep_read line 110
  16. theorem OAI.DepthThreeLowerBound.cancelByUpdates_eq_cancelStep line 132
  17. theorem OAI.DepthThreeLowerBound.reduceLoop_below line 149
  18. theorem OAI.DepthThreeLowerBound.reduceByUpdates_word_eq line 159
  19. theorem OAI.DepthThreeLowerBound.reduceByUpdates_eq_reduceLoop line 181
  20. theorem OAI.DepthThreeLowerBound.reduceByUpdates_tail_false line 188
  21. theorem OAI.DepthThreeLowerBound.wordList_wordResize_take line 200
  22. theorem OAI.DepthThreeLowerBound.reduceByUpdates_take_eq_wordReduce line 216
  23. theorem OAI.DepthThreeLowerBound.reduceByUpdates_convolve_eq_multiplyBitLists line 223
  24. theorem OAI.DepthThreeLowerBound.reduceByUpdates_convolveByUpdates_eq_multiplyBitLists line 233