OAI/Combinatorics/IndependentSets/Reduction/TargetRead.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LargeIndependentSets.TargetRead.encodeWords_eq line 14
  2. lemma OAI.LargeIndependentSets.TargetRead.read line 19
  3. lemma OAI.LargeIndependentSets.TargetRead.block_get line 23
  4. lemma OAI.LargeIndependentSets.TargetRead.read_vars line 43
  5. lemma OAI.LargeIndependentSets.TargetRead.read_clauses line 45
  6. lemma OAI.LargeIndependentSets.TargetRead.read_clause line 48
  7. lemma OAI.LargeIndependentSets.TargetRead.read_name line 56
  8. def OAI.LargeIndependentSets.TargetRead.signAt line 62
  9. lemma OAI.LargeIndependentSets.TargetRead.read_sign line 67
  10. def OAI.LargeIndependentSets.TargetRead.varsExpr line 73
  11. def OAI.LargeIndependentSets.TargetRead.clausesExpr line 74
  12. def OAI.LargeIndependentSets.TargetRead.nameExpr line 75
  13. def OAI.LargeIndependentSets.TargetRead.signExpr line 77
  14. lemma OAI.LargeIndependentSets.TargetRead.varsExpr_eval line 80
  15. lemma OAI.LargeIndependentSets.TargetRead.clausesExpr_eval line 82
  16. lemma OAI.LargeIndependentSets.TargetRead.nameExpr_eval line 84
  17. lemma OAI.LargeIndependentSets.TargetRead.signExpr_eval line 88
  18. def OAI.LargeIndependentSets.TargetRepair.bit line 101
  19. lemma OAI.LargeIndependentSets.TargetRepair.bit_eq line 102
  20. lemma OAI.LargeIndependentSets.TargetRepair.bit_decide line 103
  21. lemma OAI.LargeIndependentSets.TargetRepair.bit_ne_zero line 105
  22. abbrev OAI.LargeIndependentSets.TargetRepair.Shape line 107
  23. def OAI.LargeIndependentSets.TargetRepair.shape line 108
  24. def OAI.LargeIndependentSets.TargetRepair.shapeSat line 110
  25. def OAI.LargeIndependentSets.TargetRepair.shapeCons line 113
  26. def OAI.LargeIndependentSets.TargetRepair.repairedBit line 115
  27. lemma OAI.LargeIndependentSets.TargetRepair.shapeSat_exact line 119
  28. lemma OAI.LargeIndependentSets.TargetRepair.shapeCons_exact line 121
  29. lemma OAI.LargeIndependentSets.TargetRepair.repairedBit_exact line 124
  30. lemma OAI.LargeIndependentSets.TargetRepair.indicator_ne line 136
  31. def OAI.LargeIndependentSets.TargetRepair.shapeTest line 139
  32. lemma OAI.LargeIndependentSets.TargetRepair.shapeTest_nonzero line 151
  33. def OAI.LargeIndependentSets.TargetRepair.shapeExpr line 170
  34. lemma OAI.LargeIndependentSets.TargetRepair.shapeExpr_eval line 172
  35. def OAI.LargeIndependentSets.TargetRepair.repairExpr line 178
  36. lemma OAI.LargeIndependentSets.TargetRepair.repairExpr_eval line 180
  37. def OAI.LargeIndependentSets.TargetRepair.selectSlot line 185
  38. lemma OAI.LargeIndependentSets.TargetRepair.selectSlot_eval line 188