OAI/Combinatorics/ParityLifts/BitNormalize.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ParityWL.Complexity.decodeBits line 7
2. lemma OAI.ParityWL.Complexity.decodeBits_bits line 9
3. def OAI.ParityWL.Complexity.literalBits line 17
4. lemma OAI.ParityWL.Complexity.literalBits_injective line 19
5. def OAI.ParityWL.Complexity.literalCodec line 27
6. def OAI.ParityWL.Complexity.Formula.literalLists line 31
7. def OAI.ParityWL.Complexity.Formula.bitList line 33
8. lemma OAI.ParityWL.Complexity.Formula.bitList_parse line 36
9. lemma OAI.ParityWL.Complexity.Formula.literalLists_width line 41
10. lemma OAI.ParityWL.Complexity.nat_bits_length_le line 47
11. lemma OAI.ParityWL.Complexity.literalBits_size line 51
12. lemma OAI.ParityWL.Complexity.Formula.controlled line 58
13. lemma OAI.ParityWL.Complexity.Formula.listCNF_width line 68
14. lemma OAI.ParityWL.Complexity.Formula.listCNF_sat line 74
15. lemma OAI.ParityWL.Complexity.Formula.bitList_sat line 82
16. lemma OAI.ParityWL.Complexity.Formula.bitList_satisfiable line 95