OAI/Computability/DepthThree/RestrictionClause.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.liveClause line 17
  2. theorem OAI.DepthThreeLowerBound.mem_liveClause line 21
  3. theorem OAI.DepthThreeLowerBound.liveClause_scope_image_subset line 26
  4. theorem OAI.DepthThreeLowerBound.liveClause_width_le line 37
  5. theorem OAI.DepthThreeLowerBound.liveClause_normalized line 47
  6. def OAI.DepthThreeLowerBound.restrictClause line 53
  7. def OAI.DepthThreeLowerBound.residualClauseEval line 57
  8. theorem OAI.DepthThreeLowerBound.residualClauseEval_none line 62
  9. theorem OAI.DepthThreeLowerBound.residualClauseEval_some line 65
  10. theorem OAI.DepthThreeLowerBound.restrictClause_eval line 68
  11. theorem OAI.DepthThreeLowerBound.restrictClause_some_eq line 96
  12. theorem OAI.DepthThreeLowerBound.restrictClause_width_le line 105
  13. theorem OAI.DepthThreeLowerBound.restrictClause_normalized line 110
  14. theorem OAI.DepthThreeLowerBound.restrictClause_empty line 116
  15. def OAI.DepthThreeLowerBound.residualCNF line 121
  16. theorem OAI.DepthThreeLowerBound.residualCNF_nil line 124
  17. theorem OAI.DepthThreeLowerBound.residualCNF_cons_none line 127
  18. theorem OAI.DepthThreeLowerBound.residualCNF_cons_some line 130
  19. theorem OAI.DepthThreeLowerBound.residualCNF_eval_cons line 134
  20. def OAI.DepthThreeLowerBound.restrictCNF line 140
  21. theorem OAI.DepthThreeLowerBound.restrictCNF_eval line 143
  22. theorem OAI.DepthThreeLowerBound.restrictCNF_widthAtMost line 158
  23. theorem OAI.DepthThreeLowerBound.restrictCNF_normalized line 164