OAI/Computability/MatchingCount/StackPair.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryMatching.StackCode.pairBits line 9
  2. lemma OAI.BinaryMatching.StackCode.pairBits_length line 13
  3. def OAI.BinaryMatching.StackCode.Block.tagBody line 21
  4. def OAI.BinaryMatching.StackCode.Block.tagAll line 25
  5. lemma OAI.BinaryMatching.StackCode.Block.tagBody_runs line 27
  6. lemma OAI.BinaryMatching.StackCode.Block.pairBits_eq line 41
  7. lemma OAI.BinaryMatching.StackCode.Block.tagAll_runs line 47
  8. def OAI.BinaryMatching.StackCode.Block.pairInto line 83
  9. lemma OAI.BinaryMatching.StackCode.Block.pairInto_runs line 86
  10. def OAI.BinaryMatching.StackCode.Block.moveInto line 114
  11. lemma OAI.BinaryMatching.StackCode.Block.moveInto_runs line 117
  12. def OAI.BinaryMatching.StackCode.Block.decodeRev line 142
  13. lemma OAI.BinaryMatching.StackCode.Block.decodeRev_runs line 155