**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

Combinatorial objects have configurations which can be enumerated by algorithms, but especially for imperative programs, it is difficult to find out if they produce the correct output and donâ€™t generate duplicates. Therefore, for some of the most common combinatorial objects, namely n_Sequences, n_Permutations, n_Subsets, Powerset, Integer_Compositions, Integer_Partitions, Weak_Integer_Compositions, Derangements and Trees, this entry formalizes efficient functional programs and verifies their correctness. In addition, it provides cardinality proofs for those combinatorial objects. Some cardinalities are verified using the enumeration functions and others are shown using existing libraries including other AFP entries.

### License

### Topics

### Session Combinatorial_Enumeration_Algorithms

- Common_Lemmas
- n_Sequences
- n_Permutations
- Filter_Bool_List
- n_Subsets
- Powerset
- Integer_Partitions
- Integer_Compositions
- Weak_Integer_Compositions
- Derangements_Enum
- Trees
- Combinatorial_Enumeration_Algorithms