OAI/Combinatorics/MatchingCount/Arithmetic/BinaryNormalize.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.BinaryNormalize.normalize line 10
  2. lemma OAI.MatchingFPRAS.BinaryNormalize.normalize_nil line 11
  3. lemma OAI.MatchingFPRAS.BinaryNormalize.normalize_cons line 12
  4. lemma OAI.MatchingFPRAS.BinaryNormalize.normalize_bits line 20
  5. lemma OAI.MatchingFPRAS.BinaryNormalize.normalize_length line 36
  6. def OAI.MatchingFPRAS.BinaryNormalize.stripProgram line 39
  7. lemma OAI.MatchingFPRAS.BinaryNormalize.strip_nil line 43
  8. lemma OAI.MatchingFPRAS.BinaryNormalize.strip_true line 46
  9. lemma OAI.MatchingFPRAS.BinaryNormalize.strip_false line 49
  10. lemma OAI.MatchingFPRAS.BinaryNormalize.run_strip line 52
  11. def OAI.MatchingFPRAS.BinaryNormalize.stripRaw line 64
  12. lemma OAI.MatchingFPRAS.BinaryNormalize.stripRaw_exec line 65
  13. def OAI.MatchingFPRAS.BinaryNormalize.swap01 line 68
  14. lemma OAI.MatchingFPRAS.BinaryNormalize.reindex_swap line 69
  15. def OAI.MatchingFPRAS.BinaryNormalize.program line 78
  16. theorem OAI.MatchingFPRAS.BinaryNormalize.exec line 79