OAI/Combinatorics/MatchingCount/Tapes/TreeEncodingInjective.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatchingFPRAS.TreeData.encode_prefix_injective line 7
2. lemma OAI.MatchingFPRAS.TreeData.encode_injective line 24
3. lemma OAI.MatchingFPRAS.TreeData.ofList_injective line 27
4. lemma OAI.MatchingFPRAS.TreeData.bit_injective line 38
5. lemma OAI.MatchingFPRAS.TreeData.nat_injective line 41
6. lemma OAI.MatchingFPRAS.TreePost.sameProgram_encode line 52
7. lemma OAI.MatchingFPRAS.TreeTyped.list_encode_injective line 66
8. lemma OAI.MatchingFPRAS.TreeTyped.nat_encode_injective line 70
9. lemma OAI.MatchingFPRAS.TreeTyped.finsetNat_encode_injective line 71
10. lemma OAI.MatchingFPRAS.TreeTyped.pair_encode_injective line 77