OAI/Computability/DepthThree/SparseTestCodes.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.SparseClauseCode line 19
  2. abbrev OAI.DepthThreeLowerBound.SparseTestCode line 20
  3. def OAI.DepthThreeLowerBound.SparseClauseCode.decode line 24
  4. theorem OAI.DepthThreeLowerBound.SparseClauseCode.mem_decode line 27
  5. theorem OAI.DepthThreeLowerBound.SparseClauseCode.decode_none line 32
  6. theorem OAI.DepthThreeLowerBound.SparseClauseCode.exists_decode_of_card_le line 37
  7. theorem OAI.DepthThreeLowerBound.SparseClauseCode.exists_decode_of_normalized line 58
  8. theorem OAI.DepthThreeLowerBound.SparseClauseCode.card_eq line 63
  9. def OAI.DepthThreeLowerBound.SparseTestCode.decode line 71
  10. def OAI.DepthThreeLowerBound.SparseTestCode.eval line 79
  11. theorem OAI.DepthThreeLowerBound.SparseTestCode.decode_cons_none line 82
  12. theorem OAI.DepthThreeLowerBound.SparseTestCode.decode_cons_some line 86
  13. theorem OAI.DepthThreeLowerBound.SparseTestCode.decode_none line 91
  14. theorem OAI.DepthThreeLowerBound.SparseTestCode.eval_none line 97
  15. theorem OAI.DepthThreeLowerBound.SparseTestCode.eval_cons_empty line 101
  16. theorem OAI.DepthThreeLowerBound.SparseTestCode.exists_decode_of_normalized line 106
  17. theorem OAI.DepthThreeLowerBound.SparseTestCode.exists_eval_eq line 129
  18. theorem OAI.DepthThreeLowerBound.SparseTestCode.card_eq line 141