OAI/Computability/DepthThree/LanguageBitHashUpdates.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.hashUpdateRow line 8
  2. theorem OAI.DepthThreeLowerBound.hashUpdateRow_nil line 13
  3. theorem OAI.DepthThreeLowerBound.hashUpdateRow_step line 16
  4. theorem OAI.DepthThreeLowerBound.hashUpdateRow_length line 21
  5. theorem OAI.DepthThreeLowerBound.hashUpdateRow_append line 28
  6. theorem OAI.DepthThreeLowerBound.hashUpdateRow_getD line 37
  7. theorem OAI.DepthThreeLowerBound.hashUpdateRow_getD_self line 54
  8. theorem OAI.DepthThreeLowerBound.hashUpdateRow_getD_ne line 61
  9. def OAI.DepthThreeLowerBound.hashRowBit line 66
  10. def OAI.DepthThreeLowerBound.hashUpdateRows line 70
  11. theorem OAI.DepthThreeLowerBound.hashUpdateRows_nil line 75
  12. theorem OAI.DepthThreeLowerBound.hashUpdateRows_step line 78
  13. theorem OAI.DepthThreeLowerBound.hashUpdateRows_length line 83
  14. theorem OAI.DepthThreeLowerBound.hashUpdateRows_append line 90
  15. theorem OAI.DepthThreeLowerBound.hashUpdateRows_getD line 99
  16. theorem OAI.DepthThreeLowerBound.hashUpdateRow_range'_append line 118
  17. theorem OAI.DepthThreeLowerBound.hashUpdateRow_range'_prefix line 124
  18. theorem OAI.DepthThreeLowerBound.hashUpdateRow_range'_step line 131
  19. theorem OAI.DepthThreeLowerBound.hashUpdateRow_range'_snoc line 137
  20. theorem OAI.DepthThreeLowerBound.hashUpdateRows_range'_append line 144
  21. theorem OAI.DepthThreeLowerBound.hashUpdateRows_range'_prefix line 150
  22. theorem OAI.DepthThreeLowerBound.hashUpdateRows_range'_step line 157
  23. theorem OAI.DepthThreeLowerBound.hashUpdateRows_range'_snoc line 163
  24. theorem OAI.DepthThreeLowerBound.hashUpdateRow_range_succ line 170
  25. theorem OAI.DepthThreeLowerBound.hashUpdateRows_range_succ line 177
  26. theorem OAI.DepthThreeLowerBound.hashReadIndex_lt line 184
  27. theorem OAI.DepthThreeLowerBound.xorBits_map_single_index line 187
  28. theorem OAI.DepthThreeLowerBound.hashUpdateRows_getD_nodup line 201
  29. def OAI.DepthThreeLowerBound.hashByUpdates line 209
  30. theorem OAI.DepthThreeLowerBound.hashByUpdates_length line 212
  31. theorem OAI.DepthThreeLowerBound.hashByUpdates_getD line 215
  32. theorem OAI.DepthThreeLowerBound.hashRowBit_ofFn line 226
  33. theorem OAI.DepthThreeLowerBound.hashByUpdates_ofFn_eq line 240