OAI/Computability/DepthThree/LanguageInputBlockLists.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DepthThreeLowerBound.InputBlockKind line 10
  2. instance OAI.DepthThreeLowerBound.(instance at line 17) line 17
  3. def OAI.DepthThreeLowerBound.inputBlockOffset line 23
  4. def OAI.DepthThreeLowerBound.inputBlockLength line 29
  5. def OAI.DepthThreeLowerBound.inputBlockData line 35
  6. theorem OAI.DepthThreeLowerBound.inputBlock_end_le line 38
  7. theorem OAI.DepthThreeLowerBound.inputBlock_offset_le line 54
  8. theorem OAI.DepthThreeLowerBound.inputBlock_prefix_length line 59
  9. theorem OAI.DepthThreeLowerBound.inputBlockData_length line 64
  10. theorem OAI.DepthThreeLowerBound.inputBlock_reconstruct line 72
  11. theorem OAI.DepthThreeLowerBound.inputBlockData_getD line 86
  12. theorem OAI.DepthThreeLowerBound.inputBlockData_data_nat line 93
  13. theorem OAI.DepthThreeLowerBound.inputBlockData_data line 99
  14. theorem OAI.DepthThreeLowerBound.inputBlockData_hash_nat line 103
  15. theorem OAI.DepthThreeLowerBound.inputBlockData_hash line 108
  16. theorem OAI.DepthThreeLowerBound.inputBlockData_polynomial_nat line 113
  17. theorem OAI.DepthThreeLowerBound.inputBlockData_polynomial line 118
  18. theorem OAI.DepthThreeLowerBound.inputBlock_coefficient_index_lt line 123
  19. theorem OAI.DepthThreeLowerBound.inputBlockData_coefficients_nat line 134
  20. theorem OAI.DepthThreeLowerBound.inputBlockData_coefficients line 143