OAI/Computability/DepthThree/SparseLeafCNF.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DepthThreeLowerBound.SparseNormalization.toState line 18
2. theorem OAI.DepthThreeLowerBound.SparseNormalization.toState_valid line 23
3. theorem OAI.DepthThreeLowerBound.SparseNormalization.toState_added line 34
4. theorem OAI.DepthThreeLowerBound.SparseNormalization.toState_eval line 40
5. theorem OAI.DepthThreeLowerBound.SparseState.toCNF_normalized line 52
6. theorem OAI.DepthThreeLowerBound.SparseState.toCNF_widthAtMost line 66
7. theorem OAI.DepthThreeLowerBound.SparseState.toCNF_length line 77
8. theorem OAI.DepthThreeLowerBound.SparseState.active_card_eq_sum_sizes line 84
9. theorem OAI.DepthThreeLowerBound.SparseState.active_card_le_of_terminal line 97
10. theorem OAI.DepthThreeLowerBound.SparseState.toCNF_length_le_of_terminal line 112