OAI/Computability/MatchingCount/RawOddBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryMatching.Raw.ArgGood line 10
  2. def OAI.BinaryMatching.Raw.CutGood line 12
  3. def OAI.BinaryMatching.Raw.JoinGood line 13
  4. lemma OAI.BinaryMatching.Raw.oddExpand_good line 17
  5. lemma OAI.BinaryMatching.Raw.oddCombine_good line 35
  6. lemma OAI.BinaryMatching.Raw.vectorRep_code_bound line 43
  7. lemma OAI.BinaryMatching.Raw.matrixRep_code_bound line 52
  8. lemma OAI.BinaryMatching.Raw.cutRep_code_length line 60
  9. def OAI.BinaryMatching.Raw.oddWordBound line 64
  10. def OAI.BinaryMatching.Raw.oddBudget line 65
  11. lemma OAI.BinaryMatching.Raw.arg_code_bound line 67
  12. lemma OAI.BinaryMatching.Raw.join_code_bound line 75
  13. lemma OAI.BinaryMatching.Raw.command_code_bound line 86
  14. lemma OAI.BinaryMatching.Raw.cut_code_bound line 104
  15. lemma OAI.BinaryMatching.Raw.oddOrbit_bound line 111