OAI/Computability/DepthThree/LanguageSlice.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.parameterSlice line 11
  2. theorem OAI.DepthThreeLowerBound.parameterSlice_data line 26
  3. theorem OAI.DepthThreeLowerBound.parameterSlice_hash line 32
  4. theorem OAI.DepthThreeLowerBound.parameterSlice_polynomial line 40
  5. theorem OAI.DepthThreeLowerBound.parameterSlice_coefficient line 49
  6. theorem OAI.DepthThreeLowerBound.parameterSlice_suffix line 71
  7. def OAI.DepthThreeLowerBound.sliceParsedInput line 88
  8. def OAI.DepthThreeLowerBound.canonicalSlice line 102
  9. def OAI.DepthThreeLowerBound.canonicalSliceWord line 109
  10. theorem OAI.DepthThreeLowerBound.canonicalSliceWord_length line 117
  11. theorem OAI.DepthThreeLowerBound.canonicalSlice_first line 120
  12. theorem OAI.DepthThreeLowerBound.canonicalSlice_unused line 125
  13. theorem OAI.DepthThreeLowerBound.getD_ofFn_at line 131
  14. theorem OAI.DepthThreeLowerBound.canonicalSliceWord_fits line 135
  15. theorem OAI.DepthThreeLowerBound.decodeInput_canonicalSliceWord line 142
  16. theorem OAI.DepthThreeLowerBound.language_canonicalSliceWord line 204
  17. theorem OAI.DepthThreeLowerBound.language_ofFn_canonicalSlice line 212
  18. theorem OAI.DepthThreeLowerBound.language_canonicalSlice_quotient line 220
  19. theorem OAI.DepthThreeLowerBound.language_canonicalSlice_acceptEval line 230