OAI/Combinatorics/IndependentSets/Encoding/TargetLCExpr.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.TargetLC.eventExpr line 16
  2. def OAI.LargeIndependentSets.TargetLC.clauseExpr line 19
  3. def OAI.LargeIndependentSets.TargetLC.slotExpr line 20
  4. lemma OAI.LargeIndependentSets.TargetLC.clauseExpr_eval line 22
  5. lemma OAI.LargeIndependentSets.TargetLC.slotExpr_eval line 30
  6. def OAI.LargeIndependentSets.TargetLC.sampledNameExpr line 40
  7. def OAI.LargeIndependentSets.TargetLC.projectedBitExpr line 42
  8. lemma OAI.LargeIndependentSets.TargetLC.sampledNameExpr_eval line 45
  9. lemma OAI.LargeIndependentSets.TargetLC.projectedBitExpr_eval line 53
  10. def OAI.LargeIndependentSets.TargetLC.rankExpr line 62
  11. lemma OAI.LargeIndependentSets.TargetLC.rankExpr_eval line 64
  12. def OAI.LargeIndependentSets.TargetLC.leftExpr line 70
  13. def OAI.LargeIndependentSets.TargetLC.rightExpr line 71
  14. lemma OAI.LargeIndependentSets.TargetLC.leftExpr_eval line 72
  15. lemma OAI.LargeIndependentSets.TargetLC.rightExpr_eval line 76
  16. def OAI.LargeIndependentSets.TargetLC.projectionTest line 81
  17. lemma OAI.LargeIndependentSets.TargetLC.projectionTest_nonzero line 86
  18. def OAI.LargeIndependentSets.TargetLC.projectExpr line 98
  19. lemma OAI.LargeIndependentSets.TargetLC.projectExpr_eval line 99