OAI/Computability/DepthThree/RestrictionPaths.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.revealed line 18
  2. def OAI.DepthThreeLowerBound.residual line 21
  3. theorem OAI.DepthThreeLowerBound.revealed_nil line 24
  4. theorem OAI.DepthThreeLowerBound.mem_revealed line 27
  5. theorem OAI.DepthThreeLowerBound.revealed_subset line 31
  6. theorem OAI.DepthThreeLowerBound.revealed_mono line 37
  7. theorem OAI.DepthThreeLowerBound.revealed_snoc line 43
  8. theorem OAI.DepthThreeLowerBound.residual_eq_sdiff line 58
  9. theorem OAI.DepthThreeLowerBound.residual_eq_empty_of_mem line 68
  10. theorem OAI.DepthThreeLowerBound.card_revealed_snoc line 76
  11. def OAI.DepthThreeLowerBound.hardIndices line 86
  12. theorem OAI.DepthThreeLowerBound.mem_hardIndices line 89
  13. def OAI.DepthThreeLowerBound.paths line 100
  14. theorem OAI.DepthThreeLowerBound.paths_zero line 105
  15. theorem OAI.DepthThreeLowerBound.paths_succ line 108
  16. theorem OAI.DepthThreeLowerBound.mem_paths_zero line 112
  17. theorem OAI.DepthThreeLowerBound.mem_paths_succ line 116
  18. theorem OAI.DepthThreeLowerBound.snoc_mem_paths line 123
  19. theorem OAI.DepthThreeLowerBound.mem_paths_snoc_iff line 130
  20. theorem OAI.DepthThreeLowerBound.length_of_mem_paths line 145
  21. theorem OAI.DepthThreeLowerBound.take_mem_paths line 157
  22. theorem OAI.DepthThreeLowerBound.not_mem_of_hard line 176
  23. theorem OAI.DepthThreeLowerBound.nodup_of_mem_paths line 184
  24. theorem OAI.DepthThreeLowerBound.mul_le_revealed_card line 196
  25. theorem OAI.DepthThreeLowerBound.length_mul_le_revealed_card line 207
  26. theorem OAI.DepthThreeLowerBound.paths_eq_empty_of_card_lt line 213
  27. theorem OAI.DepthThreeLowerBound.paths_horizon_eq_empty line 221
  28. theorem OAI.DepthThreeLowerBound.sum_paths_succ line 226