OAI/Combinatorics/ParityLifts/SparseEncoding.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ParityWL.Complexity.ClauseList.mapline 7 - lemma
OAI.ParityWL.Complexity.ClauseList.map_encodeline 10 - lemma
OAI.ParityWL.Complexity.minimizeList_map_encodeline 15 - lemma
OAI.ParityWL.Complexity.sparseStep_map_encodeline 26 - def
OAI.ParityWL.Complexity.SparseTree.mapline 39 - lemma
OAI.ParityWL.Complexity.SparseTree.map_rootline 43 - lemma
OAI.ParityWL.Complexity.SparseTree.map_leavesline 46 - lemma
OAI.ParityWL.Complexity.SparseTree.map_nodesline 52 - lemma
OAI.ParityWL.Complexity.SparseTree.map_validline 58 - lemma
OAI.ParityWL.Complexity.SparseTree.map_allline 70