OAI/Computability/DepthThree/Hash.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.BinaryHash.F2 line 12
  2. abbrev OAI.DepthThreeLowerBound.BinaryHash.Data line 13
  3. abbrev OAI.DepthThreeLowerBound.BinaryHash.Seed line 14
  4. abbrev OAI.DepthThreeLowerBound.BinaryHash.Output line 15
  5. def OAI.DepthThreeLowerBound.BinaryHash.sumIndex line 17
  6. theorem OAI.DepthThreeLowerBound.BinaryHash.sumIndex_val line 20
  7. theorem OAI.DepthThreeLowerBound.BinaryHash.sumIndex_left_injective line 23
  8. def OAI.DepthThreeLowerBound.BinaryHash.hashF2 line 30
  9. theorem OAI.DepthThreeLowerBound.BinaryHash.hashF2_apply line 33
  10. theorem OAI.DepthThreeLowerBound.BinaryHash.hashF2_zero_data line 36
  11. theorem OAI.DepthThreeLowerBound.BinaryHash.hashF2_zero_seed line 41
  12. theorem OAI.DepthThreeLowerBound.BinaryHash.hashF2_add_data line 46
  13. theorem OAI.DepthThreeLowerBound.BinaryHash.hashF2_sub_data line 51
  14. theorem OAI.DepthThreeLowerBound.BinaryHash.hashF2_add_seed line 56
  15. theorem OAI.DepthThreeLowerBound.BinaryHash.hashF2_sub_seed line 61
  16. def OAI.DepthThreeLowerBound.BinaryHash.hashBool line 66
  17. theorem OAI.DepthThreeLowerBound.BinaryHash.bitValue_hashBool line 72
  18. theorem OAI.DepthThreeLowerBound.BinaryHash.bitsEquivF2_hashBool line 79