Fully Automatic, Verified Classification of all Frankl-Complete (FC(6)) Set Families

TL;DR

This paper presents a fully automated and verified method for classifying all Frankl-Complete families over a six-element set, advancing the understanding of Frankl's conjecture through comprehensive enumeration and formal proof verification.

Contribution

It provides the first complete classification of FC-families over a 6-element universe using automated, formally verified methods, extending previous partial results.

Findings

All minimal FC-families over a 6-element set are characterized.

All maximal non-FC families over a 6-element set are enumerated.

The classification is formally verified within Isabelle/HOL.

Abstract

The Frankl's conjecture, formulated in 1979. and still open, states that in every family of sets closed for unions there is an element contained in at least half of the sets. A family Fc is called Frankl-complete (or FC-family) if in every union-closed family F containing Fc, one of the elements of union Fc occurs in at least half of the elements of F (so F satisfies the Frankl's condition). FC-families play an important role in attacking the Frankl's conjecture, since they enable significant search space pruning. We extend previous work by giving a total characterization of all FC-families over a 6-element universe, by defining and enumerating all minimal FC and maximal nonFC-families. We use a fully automated, computer assisted approach, formally verified within the proof-assistant Isabelle/HOL.

Tables

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,4},{0,1,2,3,5},{1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,4},{1,2,3,4}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,4},{1,2,3,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,2,3,5},{1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{0,2,4,5},{1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,3,4,5},{1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{1,2,3,5},{0,1,2,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{1,2,4,5},{0,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{2,3,4,5},{1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,2,4,5},{1,3,4,5},{0,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{2,3,4,5},{0,1,2,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,2,5},{0,3,4,5},{1,3,4,5},{0,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,1,4,5},{2,3,4,5},{0,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,2,4,5},{0,3,4,5},{1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{2,3,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{2,3,4,5},{0,1,3,4,5},{0,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,4},{0,1,2,5},{0,1,3,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,1,3,5},{2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,4},{0,1,2,5},{0,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,2,3,5},{1,2,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,1,3,5},{0,1,4,5},{0,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,1,3,5},{0,2,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,5},{0,1,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,5},{0,1,2,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{0,1,2,3,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,1,3,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,3,4,5},{0,1,2,3,5},{0,1,2,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{2,3,4,5},{0,1,2,3,5},{0,1,2,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,3,4,5},{1,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{1,2,3,4}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{1,2,3,5}}

{{0,1,2},{0,1,3,4},{0,2,3,5},{1,2,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,5},{1,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,2,3,4},{1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,1,3,5},{0,2,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{1,3,4,5},{0,1,2,3,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{1,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{0,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,1,3,5},{2,3,4,5},{0,1,2,4,5}}

{{0,1,2},{0,1,3,4},{0,1,3,5},{2,3,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,1,3,5},{0,1,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,2,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,2,3,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,2,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{0,1,3,5},{0,1,2,4,5}}

{{0,1,2},{0,1,3,4},{0,1,3,5},{0,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,3,4,5},{0,1,2,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,3,4,5},{2,3,4,5},{0,1,2,3,5},{0,1,2,4,5}}

{{0,1,2},{0,1,3,4},{0,3,4,5},{1,3,4,5},{0,1,2,3,5},{0,1,2,4,5}}

{{0,1,2},{0,1,3,4},{0,3,4,5},{1,3,4,5},{0,1,2,3,5},{0,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,3,4,5},{2,3,4,5},{0,1,2,3,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,3,4,5},{0,1,2,3,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,3,4,5},{0,1,2,3,4},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{2,3,4,5},{0,1,2,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,3,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{2,3,4,5},{0,1,2,3,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{2,3,4,5},{0,1,2,3,4},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,2,3,4},{0,1,3,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,2,3,4},{0,1,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{0,1,3,5},{0,2,3,5}}

{{0,1,2},{0,1,3,4},{0,1,3,5},{0,1,4,5},{0,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{0,1,3,5},{0,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,2,3,4},{1,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,2,4,5},{1,3,4,5}}

{{0,1,2},{0,1,3,4},{0,1,3,5},{0,3,4,5},{1,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{0,3,4,5},{1,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,1,4,5},{0,2,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,2,3,4},{0,3,4,5},{0,1,2,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,3,4,5},{1,3,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,3,4,5},{1,3,4,5},{0,1,2,3,4}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,3,4,5},{1,3,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,3,4,5},{1,3,4,5},{0,1,2,3,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,3,4,5},{1,3,4,5},{0,1,2,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,3,4,5},{2,3,4,5},{0,1,2,3,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,3,4,5},{2,3,4,5},{0,1,2,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,3,4,5},{2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,3,4,5},{2,3,4,5},{0,1,2,3,4}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,3,4,5},{2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,1,3,5},{0,3,4,5},{0,1,2,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,1,4,5},{0,3,4,5},{0,1,2,3,5},{0,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,3,4,5},{1,3,4,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{2,3,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,5},{2,3,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,5},{2,3,4,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,3,4,5},{1,3,4,5},{0,1,2,3,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{2,3,4,5},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{0,2,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,3,5},{0,2,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,4},{0,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,2,4,5},{0,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,3,5},{2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,3,4,5},{1,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,3,4,5},{2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,3,4,5},{1,3,4,5},{2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,3,5},{0,3,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{0,3,4,5},{0,1,2,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{2,3,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,1,3,5},{0,3,4,5}}

{{0,1,2},{0,1,3},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,3,4},{1,2,3,4}}

{{0,1,2},{0,1,3},{0,2,3,4}}

{{0,1,2},{0,1,3},{0,1,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,3},{0,2,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3},{2,3,4,5},{0,2,3,4,5}}

{{0,1,2},{0,3,4},{1,2,3,5},{0,1,3,4,5}}

{{0,1,2},{0,3,4},{0,1,3,5},{0,1,2,4,5}}

{{0,1,2},{0,3,4},{0,1,3,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,2,4,5},{0,1,3,4,5},{0,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,4,5},{1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,3,4},{1,2,3,5},{0,1,2,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,2,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,2,3,4,5}}

{{0,1,2},{0,1,3},{0,2,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5}}

{{0,1,2},{0,1,3},{2,3,4,5},{0,1,2,3,4},{0,1,2,4,5},{0,1,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,5},{0,1,2,3,5},{0,1,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,4,5},{0,2,4,5}}

{{0,1,2},{0,1,3},{0,2,4,5},{1,2,4,5}}

{{0,1,2},{0,1,3},{0,2,4,5},{1,3,4,5}}

{{0,1,2},{0,1,3},{0,1,4,5},{2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{1,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,4,5}}

{{0,1,2},{3,4,5},{0,1,3,4},{0,2,3,5}}

{{0,1,2},{0,1,3},{0,1,2,4},{0,2,4,5},{0,1,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,4},{0,3,4,5},{0,1,2,3,5}}

{{0,1,2},{0,1,3},{0,1,2,4},{0,3,4,5},{0,1,2,4,5}}

{{0,1,2},{0,1,3},{0,1,2,4},{0,3,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,4},{0,2,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,4},{2,3,4,5},{0,1,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,5},{1,3,4,5},{0,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,5},{1,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{1,2,3,5},{0,1,2,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{1,2,4,5},{0,1,2,3,5}}

{{0,1,2},{0,3,4},{0,1,2,5},{1,2,3,5},{0,1,2,4,5}}

{{0,1,2},{0,3,4},{0,1,2,5},{1,2,3,5},{1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,4},{1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,3,4},{1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,3,4},{0,2,3,4},{1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,3,4},{0,2,3,4},{0,1,2,3,5}}

{{0,1,2},{0,1,3},{0,1,2,4},{2,3,4,5},{0,1,2,3,5},{0,1,2,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,3,4},{0,1,2,4,5},{0,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,3,4},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,1,2,3,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,4},{0,1,3,4},{2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,4},{0,1,2,5},{0,2,4,5}}

{{0,1,2},{0,1,3},{0,1,2,4},{0,1,3,4},{0,2,4,5}}

{{0,1,2},{0,1,3},{0,1,2,4},{0,1,3,5},{2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,3,5},{0,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,5},{0,1,3,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{1,2,3,5},{0,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{1,2,4,5},{0,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,5},{1,2,3,5},{0,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,3,4},{0,1,3,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,4},{1,2,3,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,5},{1,2,3,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,3,4},{0,1,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,3,4},{0,2,3,4}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,4,5},{0,2,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,5},{0,3,4,5},{1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,3,4},{2,3,4,5},{0,1,2,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,3,4},{0,3,4,5},{0,1,2,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,3,4},{0,1,2,5},{0,1,2,4,5},{0,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,3,4},{2,3,4,5},{0,1,2,3,5},{0,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,4,5},{2,3,4,5},{0,1,2,3,4},{0,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,4}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,1,3,4},{2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,1,3,5},{2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,4},{0,1,2,5},{0,3,4,5},{0,1,3,4,5},{0,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,3,4,5},{1,3,4,5},{0,1,2,3,5},{0,1,2,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,3,4,5},{1,3,4,5},{0,1,2,3,5},{0,2,3,4,5}}

{{0,1,2},{0,3,4},{1,3,5}}

{{0,1,2},{0,1,3},{0,4,5}}

{{0,1,2},{0,1,3},{2,3,4}}

{{0,1,2},{0,1,3},{0,2,4}}

{{0,1,2},{0,1,3},{0,1,4}}

{{0,1,2},{0,1,3},{0,2,3}}

{{0,1,2},{0,1,3},{2,4,5},{0,2,3,4,5}}

{{0,1,2},{0,1,3},{2,4,5},{0,1,2,3,4},{0,1,3,4,5}}

{{0,1,2},{0,1,3},{2,4,5},{0,2,4,5}}

{{0,1,2},{0,1,3},{2,4,5},{0,1,2,4},{0,1,2,3,5}}

{{0,1,2},{0,1,3},{2,4,5},{2,3,4,5},{0,1,2,3,4}}

{{0,1,2},{0,1,3},{2,4,5},{2,3,4,5},{0,1,3,4,5}}

{{0,1}}

{{0}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,4},{0,1,2,3,4},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,2,3,4,5},{1,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},

{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},

{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,1,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},

{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,2,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},

{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},

{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,3,4,5},{1,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},

{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{1,2,3,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{1,2,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,1,4,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,2,4,5},{1,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,1,3,5},{0,2,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,2,3,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{0,2,4,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,5},{0,1,2,3,4},{0,1,2,3,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{0,1,2,3,4},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,1,2,3,4},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{1,3,4,5},{0,1,2,3,4},{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,3,4},{0,1,2,3,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,3,4},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,3,4,5},{0,1,2,3,4},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{2,3,4,5},{0,1,2,3,4},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,3,4,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,4,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{2,3,4,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,2,3,4},{0,1,3,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,3,4,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,2,3,4,5},{1,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,3,4,5},{1,3,4,5},{0,1,2,3,4},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,3,4},{0,1,3,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,3,4,5},{1,3,4,5},{0,1,2,4,5},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,1,3,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,1,4,5},{0,2,4,5},{0,1,2,3,4},{0,1,2,4,5},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,1,4,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,4,5},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,3,4,5},{2,3,4,5},{0,1,2,3,4},{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,3,4,5},{2,3,4,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{1,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,3,4,5},{1,3,4,5},{0,1,2,3,4},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,1,3,5},{0,2,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,1,3,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,1,4,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,2,3,5},{0,1,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,3,4,5},{1,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},

{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,2,3,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},

{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,3,4},{0,2,4,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},

{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,4,5},{0,2,4,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},

{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,2,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},

{0,2,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,2,5},{0,3,4,5},{1,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,3,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},

{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,5},{0,1,4,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,2,3,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,2,3,4},{0,1,2,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{1,2,3,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,3,4},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},{1,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,3},{2,3,4,5},{0,1,2,4,5},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{1,2,4,5},{0,1,2,3,4},{0,1,2,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,5},{1,3,4,5},{0,1,2,3,4},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,3},{0,2,4,5},{0,1,2,3,4},{0,1,2,4,5},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,3},{0,2,4,5},{0,1,2,3,4},{0,1,2,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,3},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,5},{0,1,2,3,4},{0,1,2,3,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,3,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{1,2,3,5},{0,1,2,3,4},{0,1,2,3,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,3,4},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,4,5},{0,1,2,3,4},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,3},{0,1,2,4},{0,3,4,5},{0,1,2,3,4},{0,1,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,3},{0,1,2,4},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,3},{0,1,2,4},{2,3,4,5},{0,1,2,3,4},{0,1,2,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,3},{0,1,2,4},{0,2,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,5},{0,1,3,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,3,4},{0,1,3,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,3,4},{0,1,3,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,3,4},{2,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,3,4},{2,3,4,5},{0,1,2,3,4},{0,1,3,4,5},{0,2,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,4,5},{2,3,4,5},{0,1,2,3,4},{0,1,2,4,5},{0,1,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},

{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,3,4,5},{0,1,2,3,4},{0,1,3,4,5},{0,2,3,4,5},

{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,3,4},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,3,4,5},

{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,4},{0,1,2,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,4},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},

{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,3,4,5},{0,1,2,3,4},{0,1,3,4,5},

{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,3,4,5},{1,3,4,5},{0,1,2,3,4},{0,1,2,3,5},

{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,1,2,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},

{0,1,2,4,5},{1,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,1,2,3,4},{0,1,2,3,5},

{0,1,2,4,5},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{3,4,5},{0,1,2,3},{0,1,2,4},{0,1,2,5},{0,3,4,5},{0,1,2,3,4},{0,1,2,3,5},

{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,3,4},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,3,4,5},{0,1,2,3,4},

{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,1,3,5},{0,1,2,3,4},

{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,2,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{0,1,2,3},{0,1,2,4},{0,1,3,4},{0,1,2,5},{0,1,3,5},{0,1,4,5},

{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{2,4,5},{0,1,2,3},{0,1,2,4,5},{0,1,3,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{2,4,5},{0,1,2,3},{0,1,2,3,4},{0,1,2,3,5},{0,1,2,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{2,4,5},{0,1,2,3},{2,3,4,5},{0,1,2,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{2,4,5},{0,1,2,3},{0,1,2,4},{0,1,2,3,4},{0,1,2,4,5},{0,1,2,3,4,5}}

{{0,1,2},{0,1,3},{2,4,5},{0,1,2,3},{0,1,3,4},{0,1,2,3,4},{0,1,2,4,5},{0,1,2,3,4,5}}

Equations

$${\mathsf{ssn}}^{F_c,w}[]F_t$$

$${\mathsf{ssn}}^{F_c,w}(h\#t)F_t$$

$$\mathsf{ssn}{F}_{c}w\equiv {\mathsf{ssn}}^{⟨F_c⟩,w}L\{\}$$

$${\mathsf{ssn}}^{F_c,w}([],0)(F_t,s_t)$$

$${\mathsf{ssn}}^{F_c,w}((h,s_h)\#t,s_l)(F_t,s_t)$$

$${\mathsf{ssn}}^{F_c,s_w}([],0)(F_t,s_t)$$

$${\mathsf{ssn}}^{F_c,s_w}((h,s_h)\#t,s_l)(F_t,s_t)$$

$${\mathsf{ic}}_{F_c}^{s_w}h(F_t,s_t)$$

$$x_A+x_B\le 1+x_{A\cup B}.$$

$$x_B\le x_{A\cup B}.$$

$$\sum _{A\subseteq \{\overline{n}\}}{x}_A\cdot {\bar{w}}_{\{\overline{n}\}}(A)<0.$$

$$\sum _{i=0}^k{c}_i\cdot (2\cdot {\#}_a{F}_i-|F_i|)<0,$$

$$P(F\cup \{A\})⟺PF\wedge \overline{P}FA.$$

$$\mathcal{F}{\odot }_{\overline{P}}A=\{F\cup \{A\}.F\in \mathcal{F}\wedge A\notin F\wedge \overline{P}FA\}$$

$$\mathcal{F}{\odot }_{\overline{P}}F=\{\mathcal{F}{\odot }_{\overline{P}}A.A\in F\}$$

$${[l_0,\dots ,l_m+1]}_n^P={[l_0,\dots ,l_m]}_n^P{\odot }_{\overline{P}}\left(\genfrac{}{}{0ex}{}{\{\overline{n}\}}{m}\right).$$

$${\mathsf{hc}}_{\{\}}^S$$

$${\mathsf{hc}}_{\{k_0\}}^S$$

$${\mathsf{hc}}_{\{k_1\}}^S$$

$${\mathsf{hc}}_{\{k_0,k_1\}}^S$$

$${\bar{w}}_{(\bigcup F)}(F)=\sum _{K^{\prime }\subseteq K}{\bar{w}}_{K^{\prime }(\bigcup F)}^S(F).$$

$$\sum _{i=0}^k{c}_i\cdot (2\cdot {\#}_a{F}_i-|F_i|)<0,$$

$${[l_0,\dots ,l_m+1]}_n^P={[l_0,\dots ,l_m]}_n^P{\odot }_{\overline{P}}\left(\genfrac{}{}{0ex}{}{\{\overline{n}\}}{m}\right).$$

Full text

1 Introduction

Union-closed set conjecture, an elementary and fundamental statement formulated by Péter Frankl in 1979. (therefore also called Frankl’s conjecture), states that for every family of sets closed under unions, there is an element contained in at least half of the sets (or, dually, in every family of sets closed under intersections, there is an element contained in at most half of the sets). Up to the best of our knowledge, the problem is still open, and that is not because of the lack of interest — a recent survey by Bruhn and Schaudt lists more than 50 published research articles on the topic [7].

The conjecture has been confirmed for many finite special cases. For example, Bošnjak and Marković [4] proved that the conjecture holds for families such that their union has at most $m=11$ elements and Živković and Vučković [29] describes the use of computer programs to check the case of $m=12$ elements. Lo Faro [8] establishes the connection between the size of the union and the size of the minimal counter-example, proving that for any $m$ the minimal counter-example has at least $4m-1$ sets. Using results of Zivković and Vučković the conjecture is true for every family containing $n\leq 48$ sets.

It can easily be shown that if a union-closed family contains a one-element set, then that element is abundant (occurs in at least half of the sets). Similarly, one of the elements of a two-element set in a family is abundant. Unfortunately, as first shown by Renaud and Sarvate [25], the pattern breaks for a three-element set. This motivates the search for good local configurations as they enable significant search space pruning. Following Vaughan, these are sometimes called Frankl-complete families (or just FC-families). A family $F_{c}$ is an FC-family if in every union-closed family $F\supseteq F_{c}$, one of the elements of $\bigcup F_{c}$ is abundant. A FC family is called FC($n$) if its union is an $n$-element set. Most effort has been put on investigating uniform families, where all members have the same number of elements. The number FC($k$, $n$) is the minimal number $m$ such that any family containing $m$ $k$-element sets whose union is an $n$-element set is an FC-family. Poonen gives a necessary and sufficient conditions for a family to be FC [21].

As it is usually the case in finite combinatorics, even for small values of $n$, a combinatorial explosion occurs and assistance of a computer is welcome for case-analysis within proofs. The corresponding paradigm is sometimes called proof-by-evaluation or proof-by-computation. Since these are not classical mathematical results, these proofs sometimes raise controversies. We support this criticism, and advocate that the use of computer programs in classical mathematical proofs should be allowed only if the programs are formally verified.

In our previous work [15], we have applied proof-by-computation techniques and developed a fully verified algorithm that can formally prove that a given family is FC and have applied it to confirm some known uniform FC-families and to discover a new FC-family (we have shown that each family containing a four 3-element sets contained in a 7-element set is FC, i.e., that FC($3$, $7$) $\leq 4$, which, together with the lower bound on the number of 3-sets of Morris [18] gives that FC($3$, $7$) $=4$).

In this paper we extend these results by giving a fully automated and mechanically verified (within a proof assistant) characterization of all FC($n$) families for $n\leq 6$. Such characterization requires three components:

a method to prove (within a proof-assistant) that some families are FC (the technique relies on the Poonen’s Theorem [21] and was already formalized in our previous work [15]), 2. 2.

a method to prove (within a proof-assistant) that some families are not FC (the technique also relies on the Poonen’s Theorem [21], but this is the first time that it is formalized), 3. 3.

finding a list $\mathcal{F}_{c}$ of FC and a list $\mathcal{N}_{c}$ of nonFC-families that are characteristic in some sense, formally verifying (within a proof-assistant) their FC-status (i.e., proving if a family is FC or nonFC), enumerating (within a proof-assistant) all relevant families from a 6-element universe and proving that all of them are in some sense covered by some of those characteristic families i.e., that their FC-status directly follows from the status of the covering family (this technique is novel).

Finding a list of characteristic FC and nonFC-families requires lot of experimenting and checking the FC-status of many candidate families. It has recently been shown that this process can be fully automated222All FC-families classification results in the present paper were obtained prior to Pulaj’s algorithm [22] and for determining the FC status of various families we used a semi-automated procedure that is in spirit somewhat similar to Pulaj’s technique. Afterwards we fully automated the procedure, and confirmed previous results.. Namely, Pulaj recently proposed a fully automated method for determining the FC-status of an arbitrary given family [22]. The method is based on linear integer programming, and, although not integrated within a proof-assistant, it is very reliable, as it uses exact arithmetic. Even with the fully automated FC-status checking procedure, the third point requires nontrivial effort and is the main contribution of this paper (although there are well-known algorithms for exhaustive generation of non-isomorphic objects [17]).

Apart from the significance of this core result, an important contribution of this paper is to demonstrate that in the field of finite combinatorics it is possible to use computer programs to push the bounds and simplify proofs, but in a way that does not jeopardize proof correctness. On the contrary, since all statements and algorithms have been verified within the theorem prover Isabelle/HOL, the trust in our results is significantly higher than most classical pen-and-paper proofs previously published on this topic. We emphasize that many experiments may be performed by unverified tools, and only the final results need to be checked within proof-assistants (e.g., we find the list of characteristic FC and nonFC-families using unverified tools, and verify only the final list using Isabelle/HOL).

Overview of the paper

The paper is organized as follows. In the rest of this section we describe proofs by computation and discuss some related work. In Section 2 we describe Isabelle/HOL and notation that is going to be used in the paper. In Section 3 we formally introduce basic definitions related to the Frankl’s conjecture (Frankl’s condition, FC and nonFC-families, etc.). In Section 4 we give a theorem (based on Poonen’s theorem [21]) that can be used to formally prove that a family is FC and describe two different approaches for checking the conditions of that theorem (one based on a specialized, verified procedure, and one based on linear integer programming). In Section 5 we give a theorem (also based on Poonen’s theorem [21]) that can be used to formally prove that a family is nonFC. In Section 6 we describe a fully automated (unverified) procedure for checking if an arbitrary given family is FC. In Section 7 we define the notion of covering and describe properties that our characteristic families should satisfy. In Section 8 we describe methods for enumerating all families with certain properties that is used both within an automated (unverified) procedure for finding all characteristic families, and to formally show that all families are covered by the given characteristic families. In Section 9 we give a full characterization of FC(6) families, by listing all found characteristic families, and formally proving that they cover all families in $\{\!\{\overline{6}\}\!\}$. In Section 11 we draw final conclusions and discuss possible further work.

ITPs and Proofs by computation

Interactive theorem provers (sometimes called proof assistants), like Coq, Isabelle/HOL, HOL Light, etc., have made great progress in recent years. Many classical mathematical theorems have been formally proved and proof assistants have been intensively used in hardware and software verification. Several of the most important results in formal theorem proving are for the problems that require proofs with much computational content. These proofs are usually highly complex (and therefore often require justifications by formal means) since they combine classical mathematical statements with complex computing machinery (usually computer implementation of combinatorial algorithms). The corresponding paradigm is sometimes referred to as proof-by-evaluation or proof-by-computation. Probably, the most famous examples of this approach are the proofs of the Four-Color Theorem [10] and the Kepler’s conjecture [11]. One of the authors of this paper, recently used a proof-by-computation technique to give a formal proof of the Erdös-Szekeres conjecture for hexagons [14] within Isabelle/HOL.

Related work

Bruhn and Schaudt give a detailed survey of the Frankl’s conjecture [7].

The Frankl’s conjecture has also been formulated and studied as a question in lattice theory [23, 1], and in the graph theory [6].

FC-families have been introduced by Poonen [21] who gave a necessary and a sufficient condition for a family to be FC (based on weight functions). The term FC-family was coined by Vaughan [26], and they were further studied by Gao and Yu [9], Vaughan [26, 27, 28], Morris [18], Marković [16], Bošnjak and Marković [4], and Živković and Vučković [29]. Poonen [21] proved that FC($3$, $4$) = $3$. Vaughan [26, 27, 28] showed that FC($4$, $5$) $\leq 5$ and FC($4$, $6$) $\leq 10$. Morris [18] gives a full characterization of all FC($5$)-families. He proves that FC($3$, $5$)=$3$, FC($4$, $5$)=$5$. Also, he proves that FC($3$, $6$)=$4$ and $7\leq$ FC($4$, $6$) $\leq 8$. His proofs rely on computer programs, but these are not verified and not even presented in the article (as they are ,,fairly simple-minded”). In our previous work [15] we formally confirmed all these results within a theorem prover, additionally formally proving that FC($3$, $7$) $\leq 4$.

Computer-assisted computational approach was applied by Morris [18] and Živković and Vučković [29] for solving special cases of the Frankl’s conjecture. In the latter case, computations are performed by unverified Java programs.

2 Background and notation

Logic and the notation given in this paper will follow Isabelle/HOL, with some minor simplifications to make it approachable to wider audience. Isabelle/HOL [20] is a development of Higher Order Logic (HOL), and it conforms largely to everyday mathematical notation. Embedded in a theory are the types, terms and formulae of HOL. The basic types include truth values ($\mathit{bool}$), natural numbers ($\mathit{nat}$) and integers ($\mathit{int}$).

Terms are formed as in functional programming by applying functions to arguments. Following the trandition of functional programming, functions are curried. For example, $f\ x\ y$ denotes the function $f$ applied to the arguments $x$ and then $y$ (in classical mathematics notation, this would usually be denoted by $f(x,y)$).Terms may also contain $\lambda$-abstractions. For example, $\lambda x.\ x+1$ is the function that takes an argument $x$ and returns $x+1$. Let-expressions, if-expressions, and case-expressions are also supported in terms. Let expressions are of the form ”$\mathrm{let}\ x_{1}=t_{1};\ldots;x_{n}=t_{n}\ \mathrm{in}\ t$”. This expressions is equivalent to the one obtained from the term $t$ by substituting all free occurrences of the variable $x_{i}$ by the $t_{i}$. For example ”$\mathrm{let}\ x=0\ \mathrm{in}\ x+x$” is equivalent to ”$0+0$”. If expression is of the form ”$\mathit{if}\ b\ \mathrm{then}\ t_{1}\ \mathrm{else}\ t_{2}$”. Case expressions are of the form ”$\mathrm{case}\ e\ \mathrm{of}\ \mathit{pat_{1}}\Rightarrow e_{1}\ |\ \ldots\ |\ \mathit{pat_{m}}\Rightarrow e_{m}$”. This is equivalent to $e_{i}$ if $e$ matches the pattern $pat_{i}$.

Formule are terms of the type $\mathit{bool}$. Standard logical connectives ($\neg$, $\wedge$, $\vee$, $\rightarrow$ and $\longrightarrow$) are supported. Quanfiers are written using dot-notation, as $\forall x.\ P$, and $\exists x.\ P$.

New functions can be defined by recursion (either primitive or general).

Sets over type $\alpha$, type $\alpha\,\mathit{set}$, follow the usual mathematical conventions333In a strict type setting, sets containing elements of mixed types are not allowed.. In the presentation we use the term set for sets of numbers and denote these by $A$, $A^{\prime}$, …, the term family for sets of sets (i.e., object of the type $\alpha\,\mathit{set}\,\mathit{set}$) of numbers and denote these by $F$, $F^{\prime}$, …and the term collection for sets of families (i.e., object of the type $\alpha\,\mathit{set}\,\mathit{set}\,\mathit{set}$) and denote these by $\mathcal{F}$, $\mathcal{F}^{\prime}$, …. The powerset (set of all subset) of a set $A$ will denoted by ${\sf pow}\ A$. Union of sets $A$ and $B$ is denoted by $A\cup B$, and the union of all sets in a family $F$ is denoted by $\bigcup{F}$. Image of a set $A$ under a function $f$ is denoted by $f`A$. In this paper, the number of elements in a set will be denoted by $|A|$. The set $\{0,1,\ldots,n-1\}$ will be denoted by $\{\overline{n}\}$.

Lists over type $\alpha$, type $\alpha\,\mathit{list}$, come with the empty list $[\,]$, and the infix prepend constructor $\#$ (every list is either $[\,]$ or is of the form $x\;\#\;xs$ and these two cases are usually considered when defining recursive functions over lists). Standard higher order functions ${\sf map}$, ${\sf filter}$, ${\sf foldl}$ are supported and very often used for defining list operations (for details see [20]). In this paper, the N-th element of a list $l$ will be denoted by $l_{n}$ (positions are zero-based). ${\sf butlast}\ l$ denotes the list obtained from $l$ by removing its last argument. If $l$ contains natural numbers, ${\sf dec\_last}\ l$ is the list obtained from $l$ be decreasing its last element, and ${\sf inc\_nth}\ l\ n$ is the list obtained from $l$ by increasing its $n$-th element. The predicate ${\sf distinct}\ l$ checks if the list $l$ has no repated elements, and the function ${\sf remdups}\ l$ removes duplicates from the list $l$. List $[0,1,\ldots,n-1]$ will be denoted by $[\overline{n}]$.

All definitions and statements given in this paper are formalized within Isabelle/HOL444Formal proofs are available at http://argo.matf.bg.ac.rs/downloads/formalizations/FCFamilies.zip. However, in order to make the text accessible to a more general audience not familiar with Isabelle/HOL, many minor details are omitted and some imprecisions are introduced. For example, we use standard symbolic notation common in related work, although it is clear that some symbols are ambiguous. Also, in the paper some notions will be defined by only using sets, while in the formalization they are defined by using lists (to obtain executability). Statements are grouped into propositions, lemmas, and theorems. Propositions usually express simple, technical results and are printed here without proofs, while the proofs of lemmas and theorems are given in the Appendix. All sets and families are considered to be finite and this assumptions (present in Isabelle/HOL formalization) will not be explicitly stated in the rest of the paper.

3 Basic notions

Since we are only dealing with finite sets and families, without loss of generality we can restrict the domain only to natural number domains.

Definition 1

A family $F$ over $\{\overline{n}\}$ is a collection of sets such that $\bigcup F\subseteq\{\overline{n}\}$. The collection of all families over $\{\overline{n}\}$ will be denoted by $\{\!\{\overline{n}\}\!\}$.

3.1 Union-Closed Families

First we give basic definitions of union-closed families, closure under unions, and operations used to incrementally obtain closed families. Let $F_{1}\uplus F_{2}=\{A\cup B.\ A\in F_{1}\wedge B\in F_{2}\}$.

Definition 2

Let $F$ and $F_{c}$ be families.

A family $F$ is union-closed, denoted by ${\sf uc}\ F$, iff $F\uplus F=F$, (i.e. $\forall A\in F.\ \forall B\in F.\ A\cup B\in F$). A family $F$ is union-closed for $F_{c}$, denoted by ${\sf uc}_{F_{c}}\ F$, iff ${\sf uc}\ F\wedge(F\uplus F_{c}\subseteq F)$, (i.e. ${\sf uc}\ F\wedge(\forall A\in F.\ \forall B\in F_{c}.\ A\cup B\in F)$).

Union-closure of $F$ (abbr. closure)**, denoted by $\left\langle F\right\rangle$, is the minimal family of sets (in sense of inclusion) that contains $F$ and is union-closed.

Union-closure of $F$ for $F_{c}$ (abbr. closure for $F_{c}$)**, denoted by $\left\langle F\right\rangle_{F_{c}}$, is the minimal family of sets (in sense of inclusion) that contains $F$ and is union-closed for $F_{c}$.

Insert and close operation* of set $A$ to family $F$, denoted by ${\sf ic}\ A\ F$, is the family $F\cup\{A\}\cup(F\uplus\{A\})$. Insert and close operation for $F_{c}$ of set $A$ to family $F$, denoted by ${\sf ic}_{F_{c}}\ A\ F$, is the family $F\cup\{A\}\cup(F\uplus\{A\})\cup(F_{c}\uplus\{A\})$.*

The following proposition gives some trivial properties of these notions.

Proposition 1

$\left\langle F\right\rangle=\{\bigcup F^{\prime}.\ F^{\prime}\in{\sf pow}\ F-\{\{\}\}\}$** 2. 2.

$\left\langle F\cup\{A\}\right\rangle={\sf ic}\ A\ \left\langle F\right\rangle$,  $\left\langle F\cup\{A\}\right\rangle_{F_{c}}={\sf ic}_{F_{c}}\ A\ \left\langle F\right\rangle$ 3. 3.

If $F\subseteq{\sf pow}\ \bigcup F_{c}$ and ${\sf uc}_{F_{c}}\ F$ then ${\sf uc}_{\left\langle F_{c}\right\rangle}\ F$. 4. 4.

If ${\sf uc}\ F^{\prime}$ and $F\subseteq F^{\prime}$ then $\left\langle F\right\rangle\subseteq F^{\prime}$.

3.2 The Frankl’s Condition

The next definition formalizes the Frankl’s condition and the notion of FC-family.

Definition 3

Family of sets $F$ is a Frankl’s family, denoted by ${\sf frankl}\ F$, if it contains an element that satisfies the Frankl’s condition for $F$, i.e., that occurs in at least half sets in the family $F$. Formally, ${\sf frankl}\ F\ \equiv\ \exists a.\ a\in\bigcup F\ \wedge\ 2\cdot\#_{a}F\geq|F|$, where $\#_{a}F$ denotes $|\{A\in F.\ a\in A\}|$.

3.3 FC-families

Definition 4

Family of sets $F_{c}$ is an FC-family if in every union-closed family $F$ such that $F\supseteq F_{c}$ one of the elements of $\bigcup{F_{c}}$ satisfies the Frankl’s condition for $F$. Every family that is not an FC-family is called a nonFC-family.

The next propositions give some properties of FC-families.

Proposition 2

Any superset of an FC-family is an FC-family. Any subset of a nonFC-family is a nonFC-family.

Proposition 3

A family $F_{c}$ is an FC-family iff the family $F_{c}\setminus\{\{\}\}$ is an FC-family.

Proposition 4

A family $F$ is an FC-family iff its closure $\left\langle F\right\rangle$ is an FC-family.

4 Proving that a Family is FC

In this section we describe techniques that can be used to formally prove that a given family is FC. Most statements will be given without proofs, since the proofs are available in [15].

4.1 Weight Functions and Shares

We describe the central technique for proving that a family is FC, relying on characterizations of the Frankl’s condition using weights and shares introduced by Poonen [21], but adapted to work in a proof-assistant environment.

Definition 5

A function $w:X\rightarrow\mathbb{N}$ is a weight function on $A\subseteq X$, denoted by ${\sf wf}_{A}\ w$, iff $\exists a\in A.\ w(a)>0$. Weight of a set $A$ wrt. weight function $w$, denoted by $w(A)$, is the value $\sum_{a\in A}w(a)$. Weight of a family $F$ wrt. weight function $w$, denoted by $w(F)$, is the value $\sum_{A\in F}w(A)$.

An important technique for checking Frankl’s condition is averaging — family is Frankl’s if and only if there is a weight function such that weighted average of number of occurrences of all elements exceeds $|F|/2$. A more formal formulation of this claim (that uses only integers and avoids division) is given by the following Proposition.

Proposition 5

${\sf frankl}\ F\iff\exists w.\ {\sf wf}_{(\bigcup{F})}\ w\ \wedge\ 2\cdot w(F)\;\geq\;w(\bigcup{F})\cdot|F|$**

A concept that will enable a slightly more operative formulation of the previous characterization is the concept of share (again, to avoid rational numbers, definition is different from $w(A)-w(X)/2$ that is used in the literature).

Definition 6

Let $w$ be a weight function. Share of a set $A$ wrt. $w$ and a set $X$, denoted by $\bar{w}_{X}(A)$, is the value $w(A)-w(X\setminus A)=2\cdot w(A)-w(X)$. Share of a family $F$ wrt. $w$ and a set $X$, denoted by $\bar{w}_{X}(F)$, is the value $\sum_{A\in F}\bar{w}_{X}(A)$.

Example 1

Let $w$ be a function such that $w(a_{0})=1,w(a_{1})=2$, and $w(a)=0$ for all other elements. $w$ is clearly a weight function. Then, $w(\{a_{0},a_{1},a_{2}\})=3$ and $w(\{\{a_{0},a_{1}\},\{a_{1},a_{2}\},\{a_{1}\}\})=7$. Also, $\bar{w}_{\{a_{0},a_{1},a_{2}\}}(\{a_{1},a_{2}\})=2\cdot w(\{a_{1},a_{2}\})-w(\{a_{0},a_{1},a_{2}\})=4-3=1,$ and $\bar{w}_{\{a_{0},a_{1},a_{2}\}}(\{\{a_{0},a_{1}\},\{a_{1},a_{2}\},\{a_{1}\}\})=(2\cdot 3-3)+(2\cdot 2-3)+(2\cdot 2-3)=5.$

Proposition 6

$\bar{w}_{X}(F)=2\cdot w(F)-w(X)\cdot|F|$**

Proposition 7

${\sf frankl}\ F\iff\exists w.\ {\sf wf}_{(\bigcup{F})}\ w\ \wedge\ \bar{w}_{(\bigcup{F})}(F)\geq 0$**

Union-closed extensions

The next definition introduces an important notion for checking FC-families.

Definition 7

Union-closed extensions* of a family $F_{c}$ are families that are created from elements of the domain of $F_{c}$ and are union closed for $F_{c}$. Collection of all union-closed extensions is denoted by ${\sf uce}\ F_{c}$, and defined by ${\sf uce}\ F_{c}\equiv\{F.\ F\subseteq{\sf pow}\ \bigcup{F_{c}}\wedge{\sf uc}_{F_{c}}\ F\}$.*

The following theorem corresponds to first direction of Poonen’s theorem (Theorem 1 in [21]). The proof is formalized within Isabelle/HOL and its informal counterpart is given in the Appendix.

Theorem 1

A family $F_{c}$ is an FC-family if there is a weight function $w$ such that shares (wrt. $w$ and $\bigcup F_{c}$) of all union-closed extension of $F_{c}$ are nonnegative, i.e., $\forall F\in{\sf uce}\ F_{c}.\ \bar{w}_{(\bigcup{F_{c}})}(F)\geq 0$.

In the rest of this section we show two different possibilities for searching for a union-closed extension with a negative share – the first is based on a specialized algorithm, crafted specifically for this problem, while the other is based on integer linear programming and employs an integer linear programming (ILP) package or a satisfiability modulo theory (SMT) solver.

4.2 Search for Negative Shares

Theorem 1 inspires a procedure for verifying FC-families. It should take a weight function on $\bigcup{F_{c}}$ and check that all union-closed extensions of $F_{c}$ have nonnegative shares. There are only finitely many union-closed extensions, so in principle, they can all be checked. However, in order to have efficient procedure, naive checking procedure will not suffice and further steps must be taken. We now define a procedure SomeShareNegative, denoted by ${\sf ssn}\ F_{c}\ w$, such that ${\sf ssn}\ F_{c}\ w=\top$ iff there is an $F\in{\sf uce}\ F_{c}$ such that $\bar{w}_{(\bigcup{F_{c}})}(F)<0$. The procedure is based on a recursive function ${\sf ssn}^{F_{c},w}\ L_{r}\ F_{t}$ that preforms a systematic traversal of all union-closed extensions of $F_{c}$, but with pruning that significantly speeds up the search. The procedure has four parameters ($F_{c}$, $w$, $L_{r}$, and $F_{t}$) that we now describe. The two fixed parameters of the function (parameters that do not change troughout the recursive calls) are the family $F_{c}$ and the weight function $w$. If a union-closed extension of $F_{c}$ has a negative share, it must contain one or more sets with a negative share. Therefore, a list $L$ of all different subsets of $\bigcup{F_{c}}$ with negative shares is formed and each candidate family is determined by elements of $L$ that it includes. A recursive procedure creates all candidate families by processing elements of that list sequentially, either skipping them (in one recursive branch) or including them into the current candidate family $F_{t}$ (in the other recursive branch), maintaining the invariant that the current candidate family $F_{t}$ is always from ${\sf uce}\ F_{c}$. The two parameters of the recursive function ${\sf ssn}^{F_{c},w}\ L_{r}\ F_{t}$ that change during recursive calls are the remaining part of the list $L_{r}$ and the current candidate family $F_{t}$. If the current leading element of $L_{r}$ has been already included in $F_{t}$ (by earlier closure operations required to maintain the invariant) the search can be pruned. If the sum of (negative) shares of $L_{r}$ (the remaining elements of $L$) is less then the (nonnegative) share of the current $F_{t}$, then $F_{t}$ cannot be extended to a family with a negative share (even in the extreme case when all the remaining elements of $L$ are included) so, again, the search can be pruned.

Definition 8

The function ${\sf ssn}^{F_{c},w}\ L_{r}\ F_{t}$ is defined by a primitive recursion (over the structure of the list $L_{r}$):

[TABLE]

Let $L$ be a distinct list such that its set is $\{A.\ A\in{\sf pow}\ \bigcup{F_{c}}\ \wedge\ \bar{w}_{\bigcup{F_{c}}}(A)<0\}$.

[TABLE]

The soundnes of the ${\sf ssn}\ F_{c}\ w$ function is given by the following propositions.

Proposition 8

If (i) ${\sf ssn}^{F_{c},w}\ L_{r}\ F_{t}=\bot$, (ii) for all elements $A$ in $L_{r}$ it holds that $\bar{w}_{\bigcup{F_{c}}}(A)<0$, (iii) for all $A\in F-F_{t}$, if $\bar{w}_{\bigcup{F_{c}}}(A)<0$, then $A$ is in $L_{r}$, (iv) $F\supseteq F_{t}$, and (v) ${\sf uc}_{F_{c}}\ F$, then $\bar{w}_{\bigcup{F_{c}}}(F)\geq 0$.

Proposition 9

If ${\sf ssn}\ F_{c}\ w=\bot$ and $F\in{\sf uce}\ F_{c}$ then $\bar{w}_{(\bigcup{F_{c}})}(F)\geq 0$.

Apart from being sound, the procedure can also be shown to be complete. Namely, it could be shown that if ${\sf ssn}\ F_{c}\ w=\top$, then there is an $F\in{\sf uce}\ F_{c}$ such that $\bar{w}_{(\bigcup{F_{c}})}(F)<0$. This comes from the invariant that the current family $F_{t}$ in the search is always in ${\sf uce}\ F_{c}$, which is maintained by taking the closure ${\sf ic}_{F_{c}}\ h\ F_{t}$ whenever an element $h$ is added. Since this aspect of the procedure is not relevant for the rest of the proofs, it will not be formally stated nor proved. However, this can give a method for finding a counterexample family for a given weight function, that can be useful for fully automated classification of a given family (described in Section 6), that we use to find the minimal FC-families (as described in Section 7.4).

Optimizations

Important optimization to the basic ${\sf ssn}\ F_{c}\ w$ procedure is to avoid repeated computations of family shares (both for the elements of the list $L_{r}$ and the current family $F_{t}$). So, instead of accepting a list of families of sets $L_{r}$, and the current family of sets $F_{t}$, the function is modified to accept a list of ordered pairs where first component is a corresponding element of $L_{r}$, and the second component is its share (wrt. $w$ and $\bigcup{F_{c}}$), and to accept an ordered pair $(F_{t},s_{t})$ where $s_{t}$ is its family share (wrt. $w$ and $\bigcup{F_{c}}$). The summation of shares of elements in $L_{r}$ is also unnecessarily repeated. It can be avoided if the sum $s_{l}$ is passed trough the function.

[TABLE]

Another source of inefficiency is the calculation of $\bar{w}_{(\bigcup{F_{c}})}(F_{t}^{\prime})$. If performed directly based on the definition of family share for $F_{t}^{\prime}$, the sum would contain shares of all elements from $F_{t}$ and of all elements that are added to $F_{t}$ when adding $h$ and closing for $F$. However, it is already known that the sum of shares for elements of $F_{t}$ is $s_{t}$ and the implementation could benefit from this fact. Also, calculating shares of sets that are added to $F_{t}$ can be made faster. Namely, it happens that set share of a same set is calculated over and over again in different parts of the search space. So, it is much better to precompute shares of all sets from ${\sf pow}\ (\bigcup{F_{c}})$ and store them in a lookup table that will be consulted each time a set share is needed. Note that in this case there is no more need to pass the function $w$ itself, nor to calculate the domain $\bigcup{F_{c}}$, but only the lookup table, denoted by $s_{w}$.

[TABLE]

[TABLE]

We have shown that this implementation is equivalent to the starting, abstract one (it returns false iff there is a union-closed extension with a negative share).

4.3 Integer linear programming

An alternative to using a specialized, verified procedure ${\sf ssn}\ F_{c}\ w$ is to encode the existence of a union-closed extension $F$ with a negative share as a linear integer programming problem and to employ an existing solver to do the search [22]. In our case, we need to formally prove (within the Isabelle/HOL) that our characteristic FC-families are indeed FC, so the SMT solver Z3 integrated within Isabelle/HOL can be used [3].

Assume that $F_{c}$ is given and $n$ is such number that $\bigcup{F_{c}}=\{\overline{n}\}$. Each subset of $\{\overline{n}\}$ can be either included or excluded from a family $F$. There are $2^{n}$ such subsets, wich is significantly less than the number of families which is bounded above by $2^{2^{n}}$. For each set $A\subseteq\{\overline{n}\}$ we define a 0-1 integer (or Boolean) variable $x_{A}$, and its value is 1 iff the set is included in the sought family $F$ i.e., $x_{A}=1\longleftrightarrow A\in F$. We must encode that the family is union-closed, so for every two sets $A\subseteq\{\overline{n}\}$ and $B\subseteq\{\overline{n}\}$ it must hold that $A\in F$ and $B\in F$ imply that $A\cup B\in F$, that is $x_{A}=1\ \wedge\ x_{B}=1\longrightarrow x_{A\cup B}=1$, which can be encoded as

[TABLE]

Next we must encode that family is closed for $F_{c}$, so for every set $A\in F_{c}$ and $B\subseteq\{\overline{n}\}$ it must hold that $B\in F\longrightarrow A\cup B\in F$, which can be encoded as

[TABLE]

Finally, we should encode that $F$ has a negative share, i.e., $\bar{w}_{(\bigcup{F_{c}})}(F)<0$. Since $\bar{w}_{(\bigcup{F_{c}})}(F)=\sum_{A\in F}\bar{w}_{\{\overline{n}\}}(A)=\sum_{A\subseteq\{\overline{n}\}}x_{A}\cdot\bar{w}_{\{\overline{n}\}}(A)$, the condition is equivalent to

[TABLE]

The conjunction of the three listed types of linear inequalities is given to the SMT solver and it returns a model iff there is an union-closed extension of $F_{c}$ with a negative share (values of variables uniquely determine that extension $F$). The result of the SMT solver (a model, or an unsatisfiability proof) is then verified by Isabelle/HOL, yielding a fully formally verified proof [3].

Note that the problem could be stated as a problem over rational weights, but in our whole framework we considered only integers, and it turned out that the search is efficient enough.

5 Proving that a Family is not FC

Proving that a family is not an FC-family is also based on the Poonen’s theorem (Theorem 1 in [21]). The converse of our Theorem 1 also holds, and if there is no weight function satisfying the conditions of Theorem 1, then the family $F_{c}$ is not an FC-familly. However, this is hard to prove formally within Isabelle/HOL (the original Poonen’s proof uses the hyperplane separation theorem for convex sets), so we formally proved the following variant that is both easier to prove and more suitable for further application.

Theorem 2

Assume that $F_{c}$ is a union-closed family. If there exists a sequence of families $F_{0},\ldots,F_{k}$, and a sequence of natural numbers $c_{0},\ldots,c_{k}$ that:

for all $0\leq i\leq k$ it holds that $F_{i}\in{\sf uce}\ F_{c}$, 2. 2.

for every $a\in\bigcup{F_{c}}$ it holds that

[TABLE] 3. 3.

not all $c_{i}$ are zero (i.e., $\exists i.\ 0\leq i\leq k\wedge c_{i}>0$),

then the family $F_{c}$ is not an FC-family.

Major differences between this and Poonen’s original formulation are that instead of real we use only natural numbers, that instead of considering the whole collection ${\sf uce}\ F_{c}$ we consider only some of its members, and that instead of showing that there is no weight function with non-negative shares for those selected union-closed extensions i.e., showing that the system $\bar{w}_{(\bigcup{F_{c}})}(F_{i})\geq 0$ i.e., $\sum_{a\in\bigcup{F_{c}}}w_{a}\cdot(2\cdot\#_{a}F_{i}-|F_{i}|)\geq 0$, for all every $0\leq i\leq k$, has no all-nonnegative, non-all-zero solutions, we show that the its dual system $\sum_{i=0}^{k}c_{i}\cdot(2\cdot\#_{a}F_{i}-|F_{i}|)<0$, for every $a\in\bigcup{F_{c}}$, has a nontrivial solution ($2\cdot\#_{a}F_{i}-|F_{i}|$ equals the difference between the number of members of $F_{i}$ that contain $a$ and the number of members of $F_{i}$ that do not). The proof follows Poonen (to most extent) and is given in the Appendix.

Note that once the sequence of families $F_{0},\ldots,F_{k}$ and the sequence of numbers $c_{0},\ldots,c_{k}$ are known, the formal proof is much easier than in the FC case, as it need not use any search (all conditions of Theorem 2 can be directly checked). Finding those sequences is not trivial, but it can be done outside Isabelle/HOL.

6 Procedure for checking FC-status of a given family and

finding witnesses

To prove that a family is FC based on Theorem 1 one requires a witnessing weight function $w$. To prove that a family is nonFC based on Theorem 2 one requires a witnessing sequence of families $F_{i}$ and numbers $c_{i}$. For the final formal proof of the FC-status of characteristic families it is not important how those witnesses are obtained. It is very desired to have a procedure that can obtain them fully automatically. Pulaj suggested the first algorithm capable of checking the FC-status of an arbitrary family based on the cutting planes method and linear (integer) programming implemented in SCIP [22], and it can easily be modified to provide required witnesses (both for the FC and the nonFC case). Note that such procedure need not be implemented within Isabelle/HOL – its purpose is to determine the status and give witnesses that can be used for Theorem 1 or 2, which are formally checked within Isabelle/HOL.

Assume that a family $F_{c}$ is given. The procedure alternates two phases. In the first one a candidate weight function is constructed, and in the second it is checked if it satisfies the condition of Theorem 1.

In the first phase, the candidate weight function (represented by unkwowns $w_{i}$, for $0\leq i<n$) is constructed by solving a system of linear integer inequalities (as we use only natural numbers in our framework). In the beginning the system contains only conditions required for a weight function ($w_{i}\geq 0$ and $\sum_{i}w_{i}>0$), but as new families are constructed in the second phase, it is extended by the condition $\bar{w}_{(\bigcup{F_{c}})}(F_{i})\geq 0$, for each family $F_{i}$ obtained in the second phase. If the current system becomes unsatisfiable, than $F_{c}$ is not FC-family, the current set of families $F_{i}$ can be used as a witness for Theorem 2 and the coefficients $c_{i}$ are obtained by solving its dual system. Otherwise, its solution is the candidate weight function used in the second phase.

In the second phase it is checked if the weight function $w$ satisfies the conditions of Theorem 1 i.e., that there is no union-closed extension of $F_{c}$ with a negative share wrt. $w$. For this, either one of the two approaches described in Section 4.2 (either on the ${\sf ssn}\ F_{c}\ w$ procedure or solving the system of linear inequalities) can be used. If all shares are non-negative, then $F_{c}$ is an FC-family and the current weight function $w$ is used as a witness to formally prove that using Theorem 1. If it does not, than the procedure constructs a family $F_{i}$ that is in the union-closed extension of $F_{c}$ and has a negative share. That family is then added to the current set of such families and fed into the first phase again.

Unlike in the final Isabelle/HOL proofs, in the experimentation phase non-verified implementations can be used (since the final witnesses are checked again, using Isabelle/HOL). Therefore, in our implementation we have used the ILP package SCIP (the same one used in [22]) in all three cases (solving the system for finding a candidate weight, solving the system to find coefficients $c_{i}$ based on the sequence of families $F_{i}$ for which finding the weight function was shown to be impossible, and for solving the system that finds a family with a negative share wrt. the current weight function $w$), as our preliminary experiments indicated that it gives results faster then the SMT solver Z3 (when run outside Isabelle/HOL). Interestingly, the ${\sf ssn}\ F_{c}\ w$ procedure often gave a family $F_{i}$ faster then SCIP, but the overall procedure required more iterations (we assume that this can be attributed to a very regular order in which ${\sf ssn}\ F_{c}\ w$ enumerates families). One additional technique for which we noticed that significantly speeds up the convergence is to favor smaller weights i.e., to require that the weight function $w$ is minimal wrt. its sum of the weights $w_{i}$ (this was possible to obtain in SCIP by using its built-in optimization features and the objective function $\sum_{i}w_{i}$).

7 Characteristic families

In this section we introduce the notion of FC-covering and nonFC-covering that enables to determine the FC-status of all families from $\{\!\{\overline{n}\}\!\}$ from the status of just a small number of FC and nonFC-families that are characteristic in some sense (that we shall precisely define). Our goal is to give a full characterization of all $2^{2^{n}}$ families from $\{\!\{\overline{n}\}\!\}$ (i.e., for each family to determine whether it is an FC-family or a nonFC-family), and in theory that can be done by explicitly checking the status for each of them. In practice that is almost impossible since even for $n=6$ there are $2^{2^{6}}=2^{64}\approx 2\cdot 10^{19}$ families. However, (i) many of them are isomorphic and (ii) many have the same closure and (iii) many include smaller FC-families or are included in larger nonFC families – we shall show that in all those cases the FC-status can be deduced from the already known status of other families, so we base our definitions of characteristic families and covering on those facts. We shall devise methods that explicitly check the FC-status for only a minimal set of characteristic families, and after that enable us to easily get the status of every family from $\{\!\{\overline{n}\}\!\}$ by checking if they are covered by the characteristic ones.

7.1 Isomorphic families. Representing collections. Bases.

Bijective changes of the domain of a family do not affect if the family is FC.

Definition 9

Two families $F$ and $F^{\prime}$ are isomorphic (denoted by $F\cong F^{\prime}$) if there is a bijective function $f$ between $\bigcup{F}$ and $\bigcup{F^{\prime}}$ such that $f`F=F^{\prime}$.

If we consider families $\{\{a\},\{a,b,c\},\{a,c\}\}$ and $\{\{0\},\{0,1,2\},\{0,2\}\}$, they are clearly isomorphic, so we consider only families over $\{\overline{n}\}$. The family $\{\{0,1,2\},\{1,2\},\{2\}\}$ also shares the same structure with the previous two (although, that might not be so obvious, consider the bijection $0\mapsto 2,1\mapsto 0,2\mapsto 1$)), so there are also many isomorphic families over $\{\overline{n}\}$.

Obviously, isomorphism is an equivalence relation and isomorphic families share all structural properties relevant to us ($F$ is union closed iff and only if $F^{\prime}$ is, $F$ satisfies the Frankl’s condition iff $F^{\prime}$ does, the same holds for FC-family condition etc.).

Proposition 10

If $F\cong F^{\prime}$ then $F$ is an FC-family iff $F^{\prime}$ is an FC-family.

Checking if the two families in $\{\!\{\overline{n}\}\!\}$ are isomorphic

One (naive) method to check if the two given families are isomorphic is to check if the second family is among the families obtained by applying all the permutations of $[\overline{n}]$ to the first family.

Another approach can be on defining the canonical representative for each family. It can be the minimal family among the families obtained by applying all permutations in $[\overline{n}]$ to that family, where families are compared based on some fixed ordering (i.e., a lexicographic ordering, where the sets are also ordered lexicographically). Then two families are isomorphic iff they have the same canonical representative.

There are more efficient orderings and methods of finding the canonical representative, which avoid considering all permutations of $[\overline{n}]$ [5], but since we only consider the case $n=6$ where the number of permutations is rather small, we use only the naive methods.

Iso-representatives and iso-bases

If a collection of families contains many families whose structural properties should be checked, it suffices to focus only on a single representative from each isomorphism equivalence class.

Definition 10

A collection $\mathcal{F}_{b}$ iso-represents the collection $\mathcal{F}$ if for every $F\in\mathcal{F}$ there exists an $F_{b}\in\mathcal{F}_{b}$ such that $F\cong F_{b}$. If there are no $F_{1}\in\mathcal{F}_{b}$ and $F_{2}\in\mathcal{F}_{b}$ such that $F_{1}\cong F_{2}$, then $\mathcal{F}_{b}$ is a iso-base of $\mathcal{F}$.

Iso-base of a given collection can be found algorithmically. Computation can start from the given collection $\mathcal{F}$, choose its arbitrary member for a representative, move it to the resulting collection, remove it and all its permuted variants from the original collection (under a given set of permutations), and repeat this sieving process until the list becomes empty. Isabelle/HOL implementation of this procedure will be denoted by $iso\_reduce_{\mathcal{P}}\ \mathcal{F}$ and its implementation is available in our formal proof documents.

Proposition 11

If $\mathcal{P}$ is a list of permutations of $[\overline{n}]$ and if $\mathcal{F}$ is a collection of families from $\{\!\{\overline{n}\}\!\}$, then $iso\_reduce_{\mathcal{P}}\ \mathcal{F}$ iso-represents $\mathcal{F}$. If $\mathcal{P}$ contains all permutations of $[\overline{n}]$, then $iso\_reduce_{\mathcal{P}}\ \mathcal{F}$ is an iso-base of $\mathcal{F}$.

If an ordering of families is defined, another way to obtain an iso-base is to find the canonical representative of each family, and form the set of all different canonical representatives.

7.2 Irreducible families

Another technique that reduces the number of $\{\!\{\overline{n}\}\!\}$ families for which the FC-status explicitly needs to be checked is based on the fact that the FC-status of a family depends only on its closure (and not the family itself). From Proposition 4 the following immediately follows.

Proposition 12

If $\left\langle F\right\rangle=\left\langle F^{\prime}\right\rangle$ then $F$ is an FC-family iff $F^{\prime}$ is an FC-family.

Definition 11

A set $A$ is dependent on a family $F$ (denoted by $\mathit{depends}\ A\ F$) if it is a union of some of its members (i.e., if $\exists F^{\prime}.\ F^{\prime}\subseteq F\wedge F^{\prime}\neq\{\}\wedge\ A=\bigcup{F^{\prime}}$).

Proposition 13

If a set $A$ is dependent on a family $F$ then $A\in\left\langle F\right\rangle$. 2. 2.

If a set $A$ is dependent on a family $F$, then $\left\langle F\cup\{A\}\right\rangle=\left\langle F\right\rangle$.

Therefore, sets that can be expressed as unions of other sets of a family do not affect its closure. Irreducible family is obtained if all dependent sets are removed (so this family is minimal in some sense and it is a basis of its closure [13]).

Definition 12

A family is irreducible if none of its sets can be expressed as a union of some of its other members (i.e., if $\nexists\,A\in F.\,\mathit{depends}\ A\ (F\setminus\{A\})$).

For each family, an irreducible family can be obtained by removing all expressible sets, one by one until there are no more such sets. This procedure is guaranteed to terminate for finite sets.

Proposition 14

Each family $F$ has an irreducible subfamily $F^{\prime}$ such that $\left\langle F\right\rangle=\left\langle F^{\prime}\right\rangle$.

The following interesting (and non-trivial) lemma, proved in [13] and formally proved in the Appendix, shows that for all families having a same closure there is a unique irreducible family, and the previous procedure will always yield the same final answer in whatever order the sets are removed.

Lemma 1

If $F$ and $F^{\prime}$ are irreducible families and $\left\langle F\right\rangle=\left\langle F^{\prime}\right\rangle$, then $F=F^{\prime}$.

7.3 Covering

Total FC characterization of all families in $\{\!\{\overline{n}\}\!\}$ is done by defining two collections $\mathcal{F}_{c}$ and $\mathcal{N}_{c}$ such that all families in $\mathcal{F}_{c}$ are FC and that all families in $\mathcal{N}_{c}$ are nonFC, and such that the status of each given $\{\!\{\overline{n}\}\!\}$ family can easily be determined by an element of $\mathcal{F}_{c}$ or $\mathcal{N}_{c}$ (we say that the given $\{\!\{\overline{n}\}\!\}$ family is covered by $\mathcal{F}_{c}$ and $\mathcal{N}_{c}$). The following definition formalizes the notion of covering and relies on Proposition 2 and Proposition 3, Proposition 4, and some trivial properties of isomorphic families.

Definition 13

A family $F$ is FC-covered by a family $F_{c}$ (denoted by $F_{c}\vdash F$) if there exists $F_{c}^{\prime}$ such that $F_{c}^{\prime}\cong F_{c}$ and $\left\langle F\right\rangle\supseteq F_{c}^{\prime}$. A family $F$ is FC-covered by a collection of families $\mathcal{F}_{c}$ (denoted by $\mathcal{F}_{c}\vdash F$) if there is an $F_{c}\in\mathcal{F}_{c}$ such that $F$ is FC-covered by $F_{c}$ (i.e., $\exists\ F_{c}\in\mathcal{F}_{c}.\ F_{c}\vdash F$). A collection of families $\mathcal{F}$ is FC-covered by a collection of families $\mathcal{F}_{c}$ (denoted by $\mathcal{F}_{c}\vdash\mathcal{F}$) if all families $F\in\mathcal{F}$ are covered by $\mathcal{F}_{c}$ (i.e., $\forall F\in\mathcal{F}.\ \mathcal{F}_{c}\vdash F$). 2. 2.

A family $F$ is nonFC-covered by $N_{c}$ (denoted by $N_{c}\Vdash F$) if there is an $N_{c}^{\prime}$ such that $N_{c}^{\prime}\cong N_{c}$ and $\left\langle F\right\rangle\subseteq\left\langle N_{c}^{\prime}\right\rangle\cup\{\{\}\}$. A family $F$ is nonFC-covered by a collection of families $\mathcal{N}_{c}$ (denoted by $\mathcal{N}_{c}\Vdash F$) if there is an $N_{c}\in\mathcal{N}_{c}$ such that $F$ is nonFC-covered by $N_{c}$ (i.e., $\exists\ N_{c}\in\mathcal{N}_{c}.\ N_{c}\Vdash F$). A collection of families $\mathcal{F}$ is nonFC-covered by a collection of families $\mathcal{N}_{c}$ (denoted by $\mathcal{N}_{c}\Vdash\mathcal{F}$) if all families $F\in\mathcal{F}$ are covered by $\mathcal{N}_{c}$ (i.e., $\forall F\in\mathcal{F}.\ \mathcal{N}_{c}\Vdash F$). 3. 3.

A family $F$ is covered by $\mathcal{F}_{c}$ and $\mathcal{N}_{c}$ (denoted by $(\mathcal{F}_{c},\mathcal{N}_{c})\vDash F$) if it is FC-covered by $\mathcal{F}_{c}$ or it is nonFC-covered by $\mathcal{N}_{c}$. A collection of families $\mathcal{F}$ is covered by $\mathcal{F}_{c}$ and $\mathcal{N}_{c}$ (denoted by $(\mathcal{F}_{c},\mathcal{N}_{c})\vDash\mathcal{F}$) if all its families are FC-covered by $\mathcal{F}_{c}$ or nonFC-covered by $\mathcal{N}_{c}$.

The next lemma (proved in the Appendix) shows that our notion of covering guarantees that FC-covered families are FC and that nonFC-covered families are not FC.

Lemma 2

Any family $F$ that is FC-covered by an FC-family $F_{c}$ is an FC-family. 2. 2.

Any family $F$ that is nonFC-covered by a nonFC-family $N_{c}$ is not an FC-family.

An important aspect of our definition of the notion of covering is that its condition can be checked easily. First, there is only a relatively small number of possible families from $\{\!\{\overline{n}\}\!\}$ that are isomorphic to a given family in $\{\!\{\overline{n}\}\!\}$ (for example, for $\{\!\{\overline{6}\}\!\}$, these are generated by $720$ permutations of the domain). As the closure of a family can be easily effectively computed, it remains to check only if it contains one of these isomorphs, and this can be performed easily.

The following proposition gives some other easy consequences of the covering definition.

Proposition 15

Let $F\subseteq F^{\prime}$. If $\mathcal{F}_{c}\vdash F$ then $\mathcal{F}_{c}\vdash F^{\prime}$. If $\mathcal{N}_{c}\Vdash F^{\prime}$ then $\mathcal{N}_{c}\Vdash F$. 2. 2.

If $F\cong F^{\prime}$ and $F_{c}\vdash F$ then $F_{c}\vdash F^{\prime}$. If $F\cong F^{\prime}$ and $N_{c}\Vdash F$ then $N_{c}\Vdash F^{\prime}$. 3. 3.

If $F_{c}\vdash F-\{\{\}\}$, then $F_{c}\vdash F$. If $N_{c}\Vdash F-\{\{\}\}$, then $N_{c}\Vdash F$. If $(\mathcal{F}_{c},\mathcal{N}_{c})\vDash F-\{\{\}\}$, then $(\mathcal{F}_{c},\mathcal{N}_{c})\vDash F$.

Since covering is preserved by isomorphisms, to show that a collection is covered it suffices to show that its iso-base is covered, as shown by the following lemma proved in Appendix.

Lemma 3

Assume that $\mathcal{F}_{b}$ iso-represents $\mathcal{F}$. If $\mathcal{F}_{c}\vdash\mathcal{F}_{b}$, then $\mathcal{F}_{c}\vdash\mathcal{F}$. If $\mathcal{N}_{c}\Vdash\mathcal{F}_{b}$, then $\mathcal{N}_{c}\Vdash\mathcal{F}$. If $(\mathcal{F}_{c},\mathcal{N}_{c})\vDash\mathcal{F}_{b}$, then $(\mathcal{F}_{c},\mathcal{N}_{c})\vDash\mathcal{F}$.

Similarly, if two families have the same closure, even if they are not equivalent, one is covered iff the other one is.

Proposition 16

If $\left\langle F\right\rangle=\left\langle F^{\prime}\right\rangle$ then $F$ is covered by $\mathcal{F}_{c}$ and $\mathcal{N}_{c}$ iff $F^{\prime}$ is.

Therefore, the following lemma, proved in Appendix, reduces the problem of checking all families in $\{\!\{\overline{n}\}\!\}$ to checking just the irreducible ones.

Lemma 4

If all irreducible families in $\{\!\{\overline{n}\}\!\}$ are covered by $\mathcal{F}_{c}$ and $\mathcal{N}_{c}$, then all families in $\{\!\{\overline{n}\}\!\}$ are covered by $\mathcal{F}_{c}$ and $\mathcal{N}_{c}$.

7.4 Minimal FC-familes and maximal nonFC-families

We want to have as few as possible characteristic families, so we want all our characteristic families to be extreme in some sense.

Definition 14

An FC-family is minimal if it is irreducible and removing each of its sets yields a nonFC-family. 2. 2.

A nonFC-family is maximal if it is union-closed and every new set addeded yields an FC-family.

It can be easily shown that minimal and maximal families are exactly those that cannot be covered by smaller or larger families.

Proposition 17

A FC-family is minimal iff it is not FC-covered by any other family. 2. 2.

A nonFC-family is maximal iff it is not nonFC-covered by any other family.

8 Enumerating families

Next we describe efficient generic procedures for enumerating all families with certain properties. Note that all concepts in this section are generic and can be used in a wider context than checking the FC-status.

8.1 L-partitioning

In this section we develop efficient methods to enumerate all families in $\{\!\{\overline{n}\}\!\}$ that have certain properties. As it is usually the case, an inductive construction gives good results. Larger families, can be obtained from the smaller ones, by adding new sets. A good attribute of a family that can be used to control the inductive construction is the number of its members of each cardinality.

Definition 15

Let $L$ be the list $[l_{0},l_{1},\ldots,l_{m}]$. A family $F$ is $L$-partitioned if it consists of $l_{0}$ empty sets, $l_{1}$ sets with 1 element, …, and $l_{m}$ sets with $m$ elements, (i.e., $(\forall A\in F.\ |A|\leq m)\ \wedge\ (\forall i.\ 0\leq i\leq m\longrightarrow|\{A\in F.\ |A|=i\}|=l_{i})$).

Example 2

The family $\{$ $\{\}$, $\{0,1,2\}$, $\{0,1,2,3\}$, $\{0,1,2,4,5\}$, $\{0,1,3,4\}$, $\{0,1,3,5\}$, $\{0,2,3,4,5\}$, $\{0,3,4,5\}$ $\}$, is $[1,0,0,1,4,2]$-partitioned, since it contains the empty set, one 3-element set, four 4-element sets and two 5-element sets.

The number of possible members of each cardinality in a family is bounded.

Proposition 18

If a family $F\in\{\!\{\overline{n}\}\!\}$ is $[l_{0},l_{1},\ldots,l_{m}]$-partitioned, then for all $i\leq n$, $l_{i}\leq\binom{n}{i}$, and for all $i>n$, $l_{i}=0$.

There is a natural partial order between lists ($\preceq$) that corresponds to subfamily ($\subseteq$) relation of $L$-partitioned families.

Definition 16

A list $L^{\prime}=[l_{0}^{\prime},\ldots,l_{m}^{\prime}]$ is pointwise less or equal to the list $L=[l_{0},\ldots,l_{m}]$ (denoted by $L^{\prime}\preceq L$) if for all $0\leq i\leq m$, it holds that $l_{i}^{\prime}\leq l_{i}$.

The relation $\preceq$ is a partial order (reflexive, antisymmetric, and transitive), tightly connected with subfamilies (e.g., if $F$ and $F^{\prime}$ are $L$ and $L^{\prime}$ partitioned families, then $F^{\prime}\subseteq F$ implies $L^{\prime}\preceq L$).

We are often interested in enumerating all families of $\{\!\{\overline{n}\}\!\}$ that are $L$-partitioned for some given list $L$ and that satisfy some given property $P$.

Definition 17

For a given list $L$, a number $n$, and a property $P$, the collection of all $L$-partitioned families of $\{\!\{\overline{n}\}\!\}$ satisfying $P$ is denoted by ${L}_{n}^{P}$.

Our goal is to define an inductive procedure for enumerating all elements in ${L}_{n}^{P}$. It will rely on the fact that each family in $\{\!\{\overline{n}\}\!\}$ that is $[l_{0},\ldots,l_{m}+1]$ partitioned is of the form $F\cup\{A\}$ where $F$ is $[l_{0},\ldots,l_{m}]$-partitioned, $|A|=m$ and $A\subseteq\{\overline{n}\}$. Note that any other position (before $m$) could be used, but the last position has some nice properties that we shall exploit.

Instead of checking whether $F\cup\{A\}$ has the property $P$, for efficiency reasons we use the incremental approach and introduce another predicate $\overline{P}$, checking relationship between $F$ and $A$ that guarantees that $F\cup\{A\}$ will have the property $P$. Note that in our inductive construction we always extend a family $F$ by a set $A$ that is not already contained in family, and that has a greater or equal cardinality than all the family members (as we always choose the last position $m$ for induction). The following definition (and the corresponding incremental predicates) will use this condition.

Definition 18

Predicate $\overline{P}$ incrementally checks predicate $P$ if for every family $F$ and a set $A$ such that $\forall A^{\prime}\in F.\ |A|\geq|A^{\prime}|$ and $A\notin F$, it holds

[TABLE]

Example 3

If we know that all elements of a family $F$ have less than $k$ elements, to check if all elements of $F\cup\{A\}$ have less than $k$ elements it suffices to check only if $A$ has less than $k$ elements. Therefore, the predicate $\overline{P}=\lambda\ F\ A.\ |A|\leq k$ incrementally checks the predicate $P=\lambda F.\ \forall A\in F.\ |A|\leq k$.

The following construction extends all families in a collection by a given set $A$, filtering out families that already contain $A$ and families that do not satisfy the given incremental predicate $\overline{P}$.

Definition 19

$\overline{P}$-filtered product of a collection $\mathcal{F}$ and a set $A$* is defined by:*

[TABLE]

$\overline{P}$-filtered product of a collection $\mathcal{F}$ and a family $F$* is defined by*

[TABLE]

Definition 20

$\binom{\{\overline{n}\}}{m}$* denotes a collection of all $A\subseteq\{\overline{n}\}$ such that $|A|=m$.*

The following theorem is the basis for an inductive construction of ${L}_{n}^{P}$ (its proof is given in the Appendix).

Theorem 3

Assume that the predicate $\overline{P}$ incrementally checks $P$. Then

[TABLE]

In many cases instead of enumerating whole ${L}_{n}^{P}$ it suffices to enumerate its iso-representing subcollection. Again, an inductive construction can be used.

Definition 21

Predicate $\overline{P}$ is preserved by injective functions, if for all functions $f$ injective on $\bigcup F\cup A$, if $\overline{P}\ F\ A$ holds, then $\overline{P}\ (f`F)\ (f`A)$ also holds.

Theorem 4

Assume that the predicate $\overline{P}$ incrementally checks $P$ and is preserved by injective functions. If $m\leq n$ and $\mathcal{F}_{b}$ is an iso-representing subcollection of ${[l_{0},\ldots,l_{m}]}_{n}^{P}$, then $\mathcal{F}^{\prime}_{b}\equiv\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m}$ is an iso-representing subcollection of ${[l_{0},\ldots,l_{m}+1]}_{n}^{P}$.

The Theorem 4 yields an iso-representing collection (not necessarily an iso-base), so the algorithm for finding an iso-base (described in Section 7.1) should be applied, if we are interested to find an iso-base (and it is usually better to work with an iso-base since this removes redundancies).

8.2 Simple recursive enumeration

For a specific list $L$, Theorem 4 inspires the following recursive procedure.

[TABLE]

The recursion goes trough a sequence of lists, decreasing the last element if it is not zero and removing it otherwise. For example, if called for a list $[1,2,2]$, it would make a sequence of recursive calls for the lists $[1,2,1]$, $[1,2,0]$, $[1,2]$, $[1,1]$, $[1,0]$, $[1]$, $[0]$, and $[\,]$. The function returns the value corresponding to the list given as its input parameter. Values corresponding to each list are reconstructed backwards (in the return of the recursion call). In the given example, it would generate families with one empty set $[1]$, then one empty and one singleton set $[1,1]$, then one empty and two singletons $[1,2]$, then one empty, two singletons and one doubleton $[1,2,1]$, and finally the required families with one empty, two singletons, and two doubletons $[1,2,2]$. The fixed parameter $v_{[\,]}$ is the value for the empty list (the base case of the recursion), and the other fixed parameter $upd$ is the function that is used to update the value corresponding to the next list in the sequence (the return value of the recursive call) and to obtain the value corresponding to the current list (the return value of the current call). When updating the value, the function $upd$ can also take the current list into account.

The following theorem shows how can we use ${\sf enum\_rec}$ to find an iso-base of ${{L}}_{n}^{P}$ for some given list $L$, number $n$, and a predicate $P$ (its proof is outlined in the Appendix).

Theorem 5

Let $L$ be a list such that $|L|\leq n+1$. Assume that:

$P\ \{\}$* holds and $v_{[\,]}=\{\{\}\}$,* 2. 2.

$\overline{P}$* incrementally checks $P$ and is preserved by injective functions,* 3. 3.

$\mathcal{P}$* contains all permutations of $[\overline{n}]$, and $upd=\lambda\ \mathcal{F}\ L.\ iso\_reduce_{\mathcal{P}}\ (\mathcal{F}\odot_{\overline{P}}\binom{\{\overline{n}\}}{|L|-1})$.*

Then ${\sf enum\_rec}^{v_{[\,]}\,upd}\ L$ is an iso-base of ${{L}}_{n}^{P}$.

8.3 Dynamic programming enumeration

Theorem 5 gives us a way to compute an iso-base of ${L}_{n}^{P}$ for a single given list $L$. However, we often want to enumerate iso-bases of ${{L}}_{n}^{P}$ for many different lists $L$ (in an extreme case, for all possible lists $L$). In that case, a much better solution can be obtained by using dynamic programming, as many subproblems will overlap. For example, calculating both ${\sf enum\_rec}^{v_{[\,]}\,upd}\ [1,2,3]$ and ${\sf enum\_rec}^{v_{[\,]}\,upd}\ [1,2,2,1]$ will require calculation of ${\sf enum\_rec}^{v_{[\,]}\,upd}\ [1,2,2]$.

Next we present a dynamic programming algorithm that traverses all lists $L$ such that $L\preceq L_{max}$ for a given list $L_{max}$ and gathers a list of values corresponding to each of those lists. The uniform upper bound (given by the list $L_{max}$) allows easy termination proof, but in some cases we want to be able to terminate the traversal of some branches earlier (before the bound of $L_{max}$ is reached).

For example, when examining different $L$-partitions of the collection $\{\!\{\overline{n}\}\!\}$ it can be noticed that there are some partitions that contain only nonFC-families, some that contain both FC and nonFC-families and some that contain only FC-families. From Proposition 15 it follows that this property is monotonic over the relation $\preceq$.

Proposition 19

If for all $F$ in $\{\!\{\overline{n}\}\!\}$ that are $L$-partitioned it holds $\mathcal{F}_{c}\vdash F$, and if $L^{\prime}\succeq L$, then for all $F$ in $\{\!\{\overline{n}\}\!\}$ that are $L^{\prime}$-partitioned it holds that $\mathcal{F}_{c}\vdash F$. 2. 2.

If for all $F$ in $\{\!\{\overline{n}\}\!\}$ that are $L$-partitioned it holds that $\mathcal{N}_{c}\Vdash F$, and if $L^{\prime}\preceq L$, then for all $F$ in $\{\!\{\overline{n}\}\!\}$ that are $L^{\prime}$-partitioned it holds that $\mathcal{N}_{c}\Vdash F$.

When showing that all families in $\{\!\{\overline{n}\}\!\}$ are covered by $\mathcal{F}_{c}$ and $\mathcal{N}_{c}$, a good approach is to identify minimal lists $L_{F}$ such that all $L_{F}$-partitioned families in $\{\!\{\overline{n}\}\!\}$ are FC-covered by $\mathcal{F}_{c}$ and maximal lists $L_{N}$ such that all $L_{N}$-partitioned families in $\{\!\{\overline{n}\}\!\}$ are nonFC-partitioned. Then it remains only to show that all $L$-partitioned families in $\{\!\{\overline{n}\}\!\}$ are covered for lists $L$ that are between all lists $L_{N}$ and $L_{F}$. However, since our inductive construction must start from the empty family, we respect only the upper bound and show the result for lists $L$ that are below all lists in $L_{F}$.

Therefore, in our algorithm it is also allowed to exclude all lists $L^{\prime}$ such that $L^{\prime}\succeq L$ for lists $L$ for which the given predicate $stop\ L$ holds. All lists encountered during the traversed will have the same length (unlike the lists traversed by the ${\sf enum\_rec}$ function, here the shorter lists will be padded by zeros). All successive lists during the traversal must differ only by one on the last non-zero entry. If $m$ is an index such that all elements after the position $m$ in the list $L$ are zero, then the list $L$ will be used to reach lists obtained by incrementing values of list $L$ on positions greater or equal to $m$. For example, the list $[3,0,1,0,0]$ will be used to reach the lists $[3,0,2,0,0]$, $[3,0,1,1,0]$ and $[3,0,1,0,1]$.

The function ${\sf enum\_dp\_aux}$ has three fixed, and four changing parameters. First two changing parameters are the current list $L$ and the value $v$ corresponding to it. Next parameter $m$ is an index of last non-zero entry in $L$, and the final parameter $res$ is the accumulating parameter that stores the result (the list of all values corresponding to lists previously encountered during the traversal). First two fixed parameters are criteria for traversal termination (the list $L_{max}$ and the predicate $stop$), and the final fixed parameter $upd$ is the function used to calculate the value corresponding to a next lists encountered during the traversal, based on the value corresponding to the current list. If a list is obtained from the list $L$ by incrementing the value on the position $m$, its corresponding value is calculated by $upd\ v\ m$, where $v$ is the value corresponding to the list $L$.

[TABLE]

The traversal usually starts from the empty list (appropriately padded by zeros), the value $v_{[\,]}$ corresponding to it, the value $m=0$, and the empty accumulating parameter $res$. The wrapper function ${\sf enum\_dp}$ performs such initial function call for ${\sf enum\_dp\_aux}$.

[TABLE]

Finally, we can use the dynamic programming enumeration to collect iso-bases of ${L}_{n}^{P}$ for all list $L\preceq L_{max}$ that were not excluded by the given $stop$ predicate.

Theorem 6

Assume that

$\overline{P}$* incrementally checks $P$ and is preserved by injective functions,* 2. 2.

$P\ \{\}$* holds and $v_{[\,]}=\{\{\}\}$,* 3. 3.

$L_{max}$* is a list such that $|L_{max}|\leq n+1$, $\mathcal{L}_{s}$ contain lists (that all have the same length $|L_{max}|$), and $stop=\lambda\ L.\ (\exists L_{s}\in\mathcal{L}_{s}.\ L\succeq L_{s})$,* 4. 4.

$\mathcal{P}$* contains all permutations of $[\overline{n}]$, $upd=\lambda\ \mathcal{F}\ m.\ iso\_reduce_{\mathcal{P}}\ (\mathcal{F}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m})$.*

Let $X=\{L.\ L\preceq L_{max}\wedge(\nexists L_{s}\in\mathcal{L}_{s}.\ L\succeq L_{s})\}$. Then, for all $L\in X$, there exists an $\mathcal{F}_{b}\in{\sf enum\_dp}\ {L_{max}\ stop\ upd\ v_{[\,]}}$ such that $\mathcal{F}_{b}$ is an iso-base of ${L}_{n}^{P}$.

8.4 Finding characteristic families

Next, we describe a fully automated procedure that finds all characteristic families — all minimal FC-families and maximal nonFC-families that are canonical wrt. lexicographic ordering of families. Note again that this procedure needs not to be verified (we implemented it outside Isabelle/HOL). The procedure is based on the dynamic programing enumeration. During the enumeration, a collection $\mathcal{F}_{c}$ of canonical, minimal FC-families, and a collection of canonical nonFC-families $\mathcal{N}_{c}^{\prime}$ discovered so far is maintained (both are empty in the beginning). For each $L$ encountered during enumeration, a list of all canonical, irreducible, $L$-partitioned families that are not FC-covered by any family in $\mathcal{F}_{c}$ is calculated (the enumeration uses the predicate $P=\lambda F.\ \mathit{ir}\ F\ \wedge\ \neg(\mathcal{F}_{c}\vdash F)$ and $\overline{P}=\lambda\ F\ A.\ \neg\ \mathit{depends}\ A\ F\wedge\ \neg(\mathcal{F}_{c}\vdash F\cup\{A\})$ — $\overline{P}$ incrementally checks $P$ and is preserved by injective functions). The FC-status of each family in that list is examined. All newly discovered FC-families are added to $\mathcal{F}_{c}$, nonFC-families to $\mathcal{N}_{c}^{\prime}$, and the procedure continues with the next list $L$.

Since the enumeration of lists $L$ is in the lexicographic order, all discovered FC-families will be minimal (an $L$-partitioned family can be covered only by a $L^{\prime}$-partitioned familiy only if $L\succeq L^{\prime}$, and if both $L$ and $L^{\prime}$ are the same length, then $L^{\prime}$ must be lexicographically smaller than $L$).

At the end, the collection $\mathcal{N}_{c}^{\prime}$ will be an iso-base of all irreducible nonFC-families in $\{\!\{\overline{n}\}\!\}$. The collection $\mathcal{N}_{c}$ of all irreducible, cannonical, maximal nonFC-families is obtained by filtering all families in $\mathcal{N}_{c}^{\prime}$ that are covered by some other family in $\mathcal{N}_{c}^{\prime}$ and calculating union-closures.

9 FC(6) families

Applying previous procedure on $\{\!\{\overline{6}\}\!\}$ led us to the following definitions (these are the characteristic families for which we shall prove that they cover all families in $\{\!\{\overline{6}\}\!\}$).

Definition 22

$\mathcal{F}_{c}^{6}=$**

$\mathcal{N}_{c}^{6}=$**

Theorem 7

All families of $\mathcal{F}_{c}^{6}$ are FC-families. All families of $\mathcal{N}_{c}^{6}$ are nonFC-families.

Proof 1

The first part is proved by direct computation based on Theorem 1 and Proposition 9 (due to the lack of space, weights are not printed). The other part is proved by direct computation based on Theorem 2 (due to the lack of space, families $F_{i}$ and coefficients $c_{i}$ are not printed)555All data used for proofs can be found in our original proof documents, available online at http://argo.matf.bg.ac.rs/formalizations/FCFamilies.zip.

Collections $\mathcal{F}_{c}^{6}$ and $\mathcal{N}_{c}^{6}$ have some other nice properties (that we do not formally prove within Isabelle/HOL as they are not necessary for our main theorem). Every family is canonical (the smallest family in lexicographic order among the families obtained by applying all permutations of $\{\overline{n}\}$ to it, where the sets are compared first by their number of ellements, and if the number of elements is the same, then lexicographically). All families in $\mathcal{F}_{c}^{6}$ and all families in $\mathcal{N}_{c}^{6}$ are irreducible. All families in $\mathcal{F}_{c}^{6}$ are minimal FC-families i.e., no family is FC-covered by other families in $\mathcal{F}_{c}^{6}$. All families in $\mathcal{N}_{c}^{6}$ are maximal nonFC-families i.e., no family is nonFC-covered by other families in $\mathcal{N}_{c}^{6}$. Families in the table are printed as they are discovered — in lexicographic order of their $L$-partition lists.

The next lemma gives a full characterization of families of $\{\!\{\overline{6}\}\!\}$ that we call semi-uniform. These are the families such that their FC-status (whether they are FC or nonFC) is known only from the number of members of certain cardinality (and it does not depend on the arrangement of elements in these family members).

Definition 23

$\mathcal{L}_{F}=\{$* $[0,0,0,0,5,6,0]$, $[0,0,0,0,7,0,0]$, $[0,0,0,1,6,5,0]$, $[0,0,0,2,0,6,0]$,

$[0,0,0,3,0,4,0]$, $[0,0,0,3,2,3,0]$, $[0,0,0,3,3,0,0]$, $[0,0,0,4,0,0,0]$,

$[0,0,1,0,0,0,0]$, $[0,1,0,0,0,0,0]$ $\}$.*

$\mathcal{L}_{N}=\{$* $[0,0,0,0,3,6,1]$, $[0,0,0,0,4,1,1]$, $[0,0,0,1,1,6,1]$, $[0,0,0,1,2,1,1]$,*

$[0,0,0,2,0,1,1]$* $\}$.*

For example, by Theorem 7, Lemma 2, and the following lemma (Lemma 5), since $[0,0,0,0,5,6,0]\in\mathcal{L}_{F}$, it holds that if a family contains $5$ four-element, and $6$ five-element sets (all contained in a six-element set), then it is an FC-family. Similarly, since $[0,0,0,0,3,6,1]\in\mathcal{L}_{N}$ it holds that that if all sets of a family (all contained in a six-element set) have at least four elements and the family contains only up to $3$ four-element sets, $6$ five-element sets and $1$ six-element sets, then it is not an FC-family.

Lemma 5

For every list $L\in\mathcal{L}_{F}$ all $L$-partitioned families of $\{\!\{\overline{6}\}\!\}$ are FC-covered by $\mathcal{F}_{c}^{6}$. For every list $L\in\mathcal{L}_{N}$, all $L$-partitioned families of $\{\!\{\overline{6}\}\!\}$ are nonFC-covered by $\mathcal{N}_{c}^{6}$.

The proof of this lemma is available in the Appendix, and is based on generating (by applying the recursive enumeration) an iso-base of all irreducible, $L$-partitioned families (for all $L\in\mathcal{L}_{F}$) that are not covered by $\mathcal{F}_{c}^{6}$ and showing that it is empty, and on generating (again by applying the recursive enumeration) an iso-base of all irreducible, $L$-partitioned families (for all $L\in\mathcal{L}_{N}$) and showing that all its elements are covered by $\mathcal{N}_{c}^{6}$.

Lists in $\mathcal{L}_{F}$ give sufficient conditions for a family to satisfy Frankl’s condition and whenever a family extends some of these families it is know that it is an FC-family. Therefore, we can focus our attention only the families that are $L$-partitioned for lists that are less then lists in $\mathcal{L}_{F}$.

Definition 24

$\mathfrak{L}_{F}=\{L.\ L\preceq[1,6,15,20,15,6,1]\ \wedge\ \not\exists L^{\prime}\in\mathcal{L}_{F}.\ L\succeq L^{\prime}\}$**

Note that pruning is very efficient and only a very small percentage of possible lists belongs to $\mathfrak{L}_{F}$ (out of 4704 lists that do not allow empty sets, singletons and doubletons, only 296 are in $\mathfrak{L}_{F}$ — if singletons and doubletons are allowed, then there are more than a million possible lists). Therefore, most families in $\{\!\{\overline{6}\}\!\}$ are FC-families.

Moreover, as shown by the following lemma proved in the Appendix, it suffices to consider only a iso-representing set of irreducible, L-partitioned families, for $L\in\mathfrak{L}_{F}$ that contain no empty set.

Lemma 6

If for all $L\in\mathfrak{L}_{F}$, there exists a collection $\mathcal{F}^{L}_{b}$ that iso-represents ${L}_{6}^{ir}$ such that $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash\mathcal{F}^{L}_{b}$, then $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash\{\!\{\overline{6}\}\!\}$.

Finally, we can show that all families of $\{\!\{\overline{6}\}\!\}$ are covered by our collections $\mathcal{F}_{c}^{6}$ and $\mathcal{N}_{c}^{6}$. The proof is given in the Appendix, and relies on using dynamic programming enumeration to enumerate all elements of iso-bases of irreducible, L-partitioned families for $L\in\mathfrak{L}_{F}$ that contain no empty set and are not covered by $\mathcal{F}_{c}^{6}$, and then showing that all of them are covered by $\mathcal{N}_{c}^{6}$.

Theorem 8

$(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash\{\!\{\overline{6}\}\!\}$**

10 Experimental results

All experiments have been done on a notebook computer with Intel(R) Core(TM) 2.3GHz CPU with 4MB RAM memory, running Linux.

In the first phase minimal FC and maximal nonFC-families were automatically detected, as described in Section 6. The process took around 150 minutes, and most of the time was consumed by the SCIP ILP solver for checking if there is a family with the negative share wrt. the current candidate weight function. During the process, the status of 197 minimal FC families was checked, along with the status of 1125 nonFC-families (these families form an iso-base of all irreducible nonFC-families with up to six elements). Note that in the region bounded from above by $\mathcal{L}_{F}$ there are 12877 FC-families that form an iso-base of all irreducible FC-families in that region, confirming that even in that region there are much more FC than nonFC-families, and that it is very important that during enumeration all families covered by smaller FC-families are excluded, so that only minimal FC-families are explicitly checked. Possible optimizations might include switching from integer to rational weights and reducing the number of nonFC-families that need to be explicitly checked (e.g., by carefully walking along the line between maximal nonFC and minimal FC-families).

The Isabelle/HOL formalization consumes around 1,2MB organized into around 20,000 lines of Isabelle/Isar proof text (approximately a half of that are automatically generated proofs for 197 minimal FC-families and 115 maximal nonFC-families). Total proof checking time by Isabelle/HOL takes around 30 minutes. The major fraction of this time goes to checking the proofs of 197 minimal FC-families (around 6 minutes) and 115 maximal nonFC-families (around 16 minutes), and for proving that all other families are covered (around 4 minutes).

This is significantly slower than unverified programs that preform the same calculations. The big difference is due to the use of machine-integers supporting atomic bitwise-or for finding set unions (and that operation is heavily trough out the whole formalization). Therefore, the proof checking time could be significantly reduced if machine-integers were also used in Isabelle/ML (a support for this has been added to Isabelle recently [12]).

Interestingly, although proving the status of nonFC-families does not involve search and proving the status of FC-families does, it turned out that nonFC-families consume more time and that currently, the most demanding part was to prove that all witness families belong to the union-closed extension (the first point of Theorem 2).

There is much room for improving the proof checking efficiency, but we did not do that since most of time is consumed by automated classification procedure and it should be the main focus for further optimization.

11 Conclusions and Further Work

In this paper, we have described a fully automated and mechanically verified method for classifying families into Frankl-complete (FC) and non Frankl-complete (nonFC), and applied it to obtain a full characterization of all families over a six element universe.

We have shown that status of any family over the six-element universe can be easily determined by knowing the status of only a very small number of characteristic families (FC-minimal and nonFC-maximal families) and we have shown that our list of 197 FC and 115 nonFC-families covers all $2^{2^{6}}$ families over the six-element universe (their vast majority being FC). All known FC-families are confirmed and a new uniform FC-family is discovered (as a simple corollary of our classification we have that FC($4$, $6$) = $7$).

Compared to the prior pen-and-paper work [18], the computer assisted approach significantly reduces the complexity of mathematical arguments behind the proof and employs computing-machinery in doing its best — quickly enumerating and checking a large search space. This enables formulation of a general framework for checking various FC-families (and finite cases of Frankl’s conjecture), without the need of employing human intellectual resources in analyzing features of specific families.

The method fully is formalized (within Isabelle/HOL), and all our results are fully mechanically verified. Apart from achieving the highest level of trust possible, the significant contribution of the formalization is the clear separation of mathematical background and combinatorial search algorithms, not present in earlier work. Also, separation of abstract properties of search algorithms and technical details of their implementation significantly simplifies reasoning about their correctness and brings them much closer to classic mathematical audience, not inclined towards computer science. We have also shown that efficient unverified procedures (such as ILP packages or SMT solvers) can freely be used during search if they are able to produce results and certificates that are independently checked and verified by proof-assistant.

Some formalized concepts about set families (e.g., concept related to family isomorphisms or irreducibility) might be useful in other applications, out of the context of Frankl’s conjecture. The same holds for procedures for efficient enumeration of all families satisfying certain properties, that are described in Section 8.

We assume that techniques introduced in this work can be adapted to obtain a full characterization of all families over a 7-element universe, but that would require a significantly higher computing power (a cluster computer working more days). We also assume that the full classification of all families over the 8-element universe is not possible with the current approach and technology.

Methods used in this paper could be adapted to formally and automatically prove finite cases of Frankl’s conjecture. For example, Živković and Vučković have informally shown that Frankl’s conjecture holds for families $F$ such that $|\bigcup{F}|\leq 12$ [29], and now their results can be confirmed fully automatically, within a proof assistant. We also assume that the automated formalized methods developed in this paper might enable us the check the conjecture for the case $|\bigcup{F}|\leq 13$ (also assuming a high computing power).

Appendix A Proofs of lemmas and theorems

A.1 Proof of Theorem 1

In this section we describe proof of Theorem 1. First we introduce some auxiliary notions.

Hypercubes

Sets of a family can be grouped into so called hypercubes.

Definition 25

An $S$-hypercube with a base $K$, denoted by ${\sf hc}_{K}^{S}$, is the family $\{A.\ K\subseteq A\wedge A\subseteq K\cup S\}$. Alternatively, a hypercube can be characterized by ${\sf hc}_{K}^{S}=\{K\cup A.\ A\in{\sf pow}\ S\}$.

Example 4

*Let $S\equiv\{s_{0},s_{1}\}$, and $K\equiv\{k_{0},k_{1}\}$. If $K^{\prime}\subseteq K$, then all $S$-hypercubes with a base $K^{\prime}$ are: *

[TABLE]

Previous example indicates that (disjoint) $S$-hypercubes can span the whole ${\sf pow}\ (K\cup S)$. Indeed, this is generally the case.

Proposition 20

(i) ${\sf pow}\ (K\cup S)=\bigcup_{K^{\prime}\subseteq K}{\sf hc}_{K^{\prime}}^{S}$. (ii) If $K_{1}$ and $K_{2}$ are different and disjoint with $S$, then ${\sf hc}_{K_{1}}^{S}$ and ${\sf hc}_{K_{2}}^{S}$ are disjoint.

Families of sets can be separated into (disjoint) parts belonging to different hypercubes (formed as ${\sf hc}_{K}^{S}\cap F$).

Definition 26

A hyper-share of a family $F$ wrt. weight function $w$, the hypercube ${\sf hc}_{K}^{S}$ and the set $X$, denoted by $\bar{w}^{S}_{KX}(F)$, is the value $\sum_{A\in{\sf hc}_{K}^{S}\cap F}\bar{w}_{X}(A)$.

Example 5

Let $S$ and $K$ be as in the Example 4, let $X\equiv K\cup S$, let $F\equiv\{\{s_{0}\},\{s_{1}\},\{k_{0},s_{0}\},\{k_{0},k_{1},s_{0},s_{1}\}\}$, and $w(a)=1$ for all $a\in X$. Then, $\bar{w}^{S}_{\{\}X}(F)=\bar{w}_{X}(\{s_{0}\})+\bar{w}_{X}(\{s_{1}\})=-4$, $\bar{w}^{S}_{\{k_{0}\}X}(F)=\bar{w}_{X}(\{k_{0},s_{0}\})=0$, $\bar{w}^{S}_{\{k_{1}\}X}(F)=0$, and $\bar{w}^{S}_{\{k_{0},k_{1}\}X}(F)$ $=$ $\bar{w}_{X}(\{k_{0},k_{1},s_{0},s_{1}\})=4$.

Share of a family can be expressed in terms of sum of hyper-shares.

Proposition 21

If $K\cup S=\bigcup{F}$ and $K\cap S=\{\}$, then

[TABLE]

Proposition 22

Let $w$ be a weight function on $\bigcup{F}$. If $K\cup S=\bigcup{F}$, $K\cap S=\{\}$, and $\forall K^{\prime}\subseteq K.\ \bar{w}^{S}_{K^{\prime}(\bigcup{F})}(F)\geq 0$, then ${\sf frankl}\ F$.

Definition 27

Projection of a family $F$ onto a hypercube ${\sf hc}_{K}^{S}$**, denoted by ${\sf hc}_{K}^{S}\left\lfloor{F}\right\rfloor$, is the set $\{A-K.\ A\in{\sf hc}_{K}^{S}\cap F\}$.

Example 6

Let $K$, $S$ and $F$ be as in Example 5. Then ${\sf hc}_{\{\}}^{S}\left\lfloor{F}\right\rfloor=\{\{s_{0}\},\{s_{1}\}\}$, ${\sf hc}_{\{k_{0}\}}^{S}\left\lfloor{F}\right\rfloor=\{\{s_{0}\}\}$, ${\sf hc}_{\{k_{1}\}}^{S}\left\lfloor{F}\right\rfloor=\{\}$, and ${\sf hc}_{\{k_{0},k_{1}\}}^{S}\left\lfloor{F}\right\rfloor=\{\{s_{0},s_{1}\}\}$.

Proposition 23

If $K\cap S=\{\}$ and $K^{\prime}\subseteq K$, then ${\sf hc}_{K^{\prime}}^{S}\left\lfloor{F}\right\rfloor\subseteq{\sf pow}\ S$ 2. 2.

If ${\sf uc}\ F$, then ${\sf uc}\ ({\sf hc}_{K}^{S}\left\lfloor{F}\right\rfloor)$. 3. 3.

If ${\sf uc}\ F$, $F_{c}\subseteq F$, $S=\bigcup F_{c}$, $K\cap S=\{\}$, then ${\sf uc}_{F_{c}}\ ({\sf hc}_{K}^{S}\left\lfloor{F}\right\rfloor)$. 4. 4.

If $\forall x\in K.\ w(x)=0$, then $\bar{w}^{S}_{KX}(F)=\bar{w}_{X}({\sf hc}_{K}^{S}\left\lfloor{F}\right\rfloor)$.

Lemma 7

Let $F$ be a non-empty union-closed family, and let $F_{c}$ be a subfamily (i.e., $F_{c}\subseteq F$). Let $w$ be a weight function on $\bigcup{F}$, that is zero for all elements of $\bigcup{F}-\bigcup{F_{c}}$. If shares of all union-closed extensions of $F_{c}$ are nonnegative, then there is an element $a\in\bigcup{F_{c}}\subseteq\bigcup{F}$ such that it satisfies the Frankl’s condition for $F$, i.e., if $\forall F^{\prime}\in{\sf uce}\ F_{c}.\ \bar{w}_{(\bigcup{F_{c}})}(F^{\prime})\geq 0$, then ${\sf frankl}\ F$.

Proof 2

Let $S$ denote $\bigcup{F_{c}}$, and let $K$ denote $\bigcup{F}-\bigcup{F_{c}}$. Since, $K\cup S=\bigcup F$ and $K\cap S=\{\}$, by Proposition 22, it suffices to show that $\forall K^{\prime}\subseteq K.\ \bar{w}^{S}_{K^{\prime}(\bigcup{F})}(F)\geq 0$. Fix $K^{\prime}$ and assume that $K^{\prime}\subseteq K$. Since $w$ is zero on $K$, by Proposition 23, it holds that $\bar{w}^{S}_{K^{\prime}(\bigcup{F})}(F)=\bar{w}_{(\bigcup{F})}({\sf hc}_{K^{\prime}}^{S}\left\lfloor{F}\right\rfloor)$. On the other hand, since ${\sf uc}\ F$, $F_{c}\subseteq F$, and $K\cap S=\{\}$, by Proposition 23 it holds that ${\sf uc}_{F_{c}}\ ({\sf hc}_{K^{\prime}}^{S}\left\lfloor{F}\right\rfloor)$. Moreover, ${\sf hc}_{K^{\prime}}^{S}\left\lfloor{F}\right\rfloor\subseteq{\sf pow}\ S$, so ${\sf hc}_{K^{\prime}}^{S}\left\lfloor{F}\right\rfloor\in{\sf uce}\ F_{c}$. Then, $\bar{w}_{(\bigcup{F_{c}})}({\sf hc}_{K^{\prime}}^{S}\left\lfloor{F}\right\rfloor)\geq 0$ holds from the assumption. However, since $w$ is zero on $K$, it holds that $w(\bigcup{F_{c}})=w(\bigcup{F})$ and $\bar{w}_{(\bigcup{F})}({\sf hc}_{K^{\prime}}^{S}\left\lfloor{F}\right\rfloor)=\bar{w}_{(\bigcup{F_{c}})}({\sf hc}_{K^{\prime}}^{S}\left\lfloor{F}\right\rfloor)\geq 0$

Finally, we can easily prove Theorem 1.

Theorem 1

A family $F_{c}$ is an FC-family if there is a weight function $w$ such that shares (wrt. $w$ and $\bigcup F_{c}$) of all union-closed extension of $F_{c}$ are nonnegative.

Proof 3

Consider an arbitrary union-closed family $F\supseteq F_{c}$. Let $w$ be the weight function such that $\forall F^{\prime}\in{\sf uce}\ F_{c}.\ \bar{w}_{(\bigcup{F_{c}})}(F^{\prime})\geq 0$. Let $w^{\prime}$ be a function equal to $w$ on $\bigcup F_{c}$ and 0 on other elements. Since $\forall F^{\prime}\in{\sf uce}\ F_{c}.\ \bar{w^{\prime}}_{(\bigcup{F_{c}})}(F^{\prime})=\bar{w}_{(\bigcup{F_{c}})}(F^{\prime})$, Lemma 7 applies to $F$ and there is an element $a\in\bigcup{F_{c}}$ that satisfies the Frankl’s condition for $F$. Therefore, $F_{c}$ is an FC-family.

A.2 Proof of Theorem 2

Theorem 2

Assume that $F_{c}$ is a union-closed family. If there exists a sequence of families $F_{0},\ldots,F_{k}$, and a sequence of natural numbers $c_{0},\ldots,c_{k}$ that:

for all $0\leq i\leq k$ it holds that $F_{i}\in{\sf uce}\ F_{c}$, 2. 2.

for every $a\in\bigcup{F_{c}}$ it holds that

[TABLE] 3. 3.

not all $c_{i}$ are zero (i.e., $\exists i.\ 0\leq i\leq k\wedge c_{i}>0$),

then the family $F_{c}$ is not an FC-family.

Proof 4

Let $c=\sum_{i=0}^{k}c_{i}$. From the assumptions, it holds that $c>0$. For each natural number $d>0$, let $B^{d}=\{b_{0},\ldots,b_{c\cdot d}\}$ be a set containing $c\cdot d+1$ elements, having no common elements with $\bigcup{F_{c}}$. For each $0\leq s<c\cdot d$, let $B^{d}_{s}=B^{d}\setminus\{b_{s}\}$. Let $G^{d}$ be a sequence of sets $[F_{1},\ldots,F_{1},F_{2},\ldots,F_{2},\ldots,F_{k},\ldots,F_{k}]$, where each $F_{i}$ is repeated exactly $c_{i}\cdot d$ times, and for each $0\leq s<c\cdot d$, let $G^{d}_{s}$ be the $s$-the member of the sequence $G^{d}$. For each $0\leq s<c\cdot d$, let $H^{d}_{s}=\{A\cup B^{d}_{s}.\ A\in G^{d}_{s}\}$. Let $H^{d}=\{A\cup B^{d}.\ A\in{\sf pow}\ \bigcup{F_{c}}\}$. Finally, we form a family $F^{d}=F_{c}\cup(\bigcup_{0\leq s<c\cdot d}H^{d}_{s})\cup H^{d}$. For an appropriately chosen $d$ it will be a counterexample that $F_{c}$ is an FC-family.

For each $d$, the family $F^{d}$ is union-closed ($F_{c}$ is union closed, so the union of each two sets from $F_{c}$ is in $F_{c}$, $H^{d}$ is also union-closed, so the union of each two sets from $F_{c}$ is in $H^{d}$, the union of each two sets from $\bigcup_{0\leq s<c\cdot d}H^{d}_{s}$ is in $H^{d}$, unions of sets from $F_{c}$ and $\bigcup_{0\leq s<c\cdot d}H^{d}_{s}$ are in $\bigcup_{0\leq s<c\cdot d}H^{d}_{s}$ since for some $i$, it holds that $G^{d}_{s}=F_{i}\in{\sf uce}\ F_{c}$, unions of sets from $F_{c}$ and $H^{d}$ are in $H^{d}$ and unions of sets from $\bigcup_{0\leq s<c\cdot d}H^{d}_{s}$ and $H^{d}$ are in $H^{d}$).

Let $f$ be a function defined by $f\ a\ F=2\cdot\#_{a}F-|F|$. Since $B^{d}$ and $\bigcup{F_{c}}$ are disjoint, for each $a\in\bigcup{F_{c}}$, $d>0$ and $0\leq s<c\cdot d$ it holds that $f\ a\ H^{d}_{s}=f\ a\ G^{d}_{s}$. As $H^{d}$ is built around the whole ${\sf pow}\ \bigcup{F_{c}}$, it can be easilly shown that for each $a\in\bigcup{F_{c}}$ and $d>0$, it holds that $f\ a\ H^{d}=0$. For each $d>0$, the families $F_{c}$, $\bigcup_{0\leq s<c\cdot d}H^{d}_{s}$, and $H^{d}$ are mutually disjoint (all $B^{d}_{s}$ are non-empty, sets in $F_{c}$ contain no element from $B^{d}$, sets from $\bigcup_{0\leq s<c\cdot d}H^{d}_{s}$ contain all but one element from $B^{d}$, while sets from $H^{d}$ contain the whole $B^{d}$). Also, for each $0\leq s_{1}\neq s_{2}<c\cdot d$, the families $H^{d}_{s_{1}}$ and $H^{d}_{s_{2}}$ are disjoint (as all sets from $H^{d}_{s_{1}}$ contain $b_{s_{2}}$, while none of the sets from $H^{d}_{s_{2}}$ does). Therefore, for each $a\in\bigcup{F_{c}}$ and $d>0$, $f\ a\ F^{d}=f\ a\ F_{c}+f\ a\ (\bigcup_{0\leq s<c\cdot d}H^{d}_{s})+f\ a\ H^{d}=f\ a\ F_{c}+\sum_{0\leq s<c\cdot d}f\ a\ G^{d}_{s}=f\ a\ F_{c}+d\cdot\sum_{0\leq s<c}f\ a\ G^{d}_{s\cdot d}$. By construction of $G^{d}$, it holds that for each $0\leq i\leq k$, the last sum has exactly $c_{i}$ terms $f\ a\ F_{i}$. Therefore, $f\ a\ F^{d}=f\ a\ F_{c}+d\cdot(\sum_{0\leq i\leq k}c_{i}\cdot(f\ a\ F_{i}))$. By assumption, $\sum_{0\leq i\leq k}c_{i}\cdot(f\ a\ F_{i})=\sum_{0\leq i\leq k}c_{i}\cdot(2\cdot\#_{a}F_{i}-|F_{i}|)$ is negative. Therefore, for each $a$, there exists a $d_{a}>0$ such that $f\ a\ F^{d_{a}}<0$. Let $d$ maximal $d_{a}$ for $a\in\bigcup{F_{c}}$. It holds that $F^{d}$ is a union-closed family containing $F_{c}$, such that each $a\in\bigcup{F_{c}}$ it holds that $f\ a\ F^{d}=(2\cdot\#_{a}F^{d}-|F^{d}|)<0$, i.e., $\#_{a}F^{d}<|F^{d}|/2$. This shows that $F_{c}$ cannot be an FC-family.

A.3 Proof of Theorem 3

Theorem 3

Assume that the predicate $\overline{P}$ incrementally checks $P$. Then

[TABLE]

Proof 5

First we show that ${[l_{0},\ldots,l_{m}+1]}_{n}^{P}\subseteq{[l_{0},\ldots,l_{m}]}_{n}^{P}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m}$. Let $F^{\prime}$ be an arbitrary family in ${[l_{0},\ldots,l_{m}+1]}_{n}^{P}$. Then $F^{\prime}$ is $[l_{0},\ldots,l_{m}+1]$-partitioned, $\bigcup F^{\prime}\subseteq\{\overline{n}\}$, and $P\ F^{\prime}$ holds. Since $l_{m}+1>0$, there is an element $A\in F^{\prime}$ such that $|A|=m$. Since $\bigcup F^{\prime}\subseteq\{\overline{n}\}$ and $A\in F^{\prime}$, it holds that $A\subseteq\{\overline{n}\}$, so $A\in\binom{\{\overline{n}\}}{m}$. Let $F$ denote the set $F^{\prime}\setminus\{A\}$. Since $A\in F^{\prime}$, it holds that $F^{\prime}=F\cup\{A\}$. Since $\overline{P}$ incrementally checks $P$, and since for all $A^{\prime}\in F^{\prime}$, it holds that $|A|=m\geq|A^{\prime}|$, and since $A\notin F$, from $P\ F^{\prime}$, by relation (1) it holds that $P\ F$ and $\overline{P}\ F\ A$. The set $F$ is in ${[l_{0},\ldots,l_{m}]}_{n}^{P}$. Indeed, it is $[l_{0},\ldots,l_{m}]$-partitioned, it holds that $\bigcup F\subseteq\bigcup F^{\prime}\subseteq\{\overline{n}\}$, and $P\ F$ holds. Since $A\in\binom{\{\overline{n}\}}{m}$, $A\notin F$ and $\overline{P}\ F\ A$, by the definition of $\overline{P}$-filtered multiplication $F^{\prime}$ is in ${[l_{0},\ldots,l_{m}]}_{n}^{P}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m}$.

To prove ${[l_{0},\ldots,l_{m}+1]}_{n}^{P}\supseteq{[l_{0},\ldots,l_{m}]}_{n}^{P}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m}$, assume that $F^{\prime}$ is an arbitrary element of ${[l_{0},\ldots,l_{m}]}_{n}^{P}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m}$. Then there is an element $F\in{[l_{0},\ldots,l_{m}]}_{n}^{P}$ and $A\in\binom{\{\overline{n}\}}{m}$ such that $F^{\prime}=F\cup\{A\}$, $A\notin F$, and $\overline{P}\ F\ A$. Therefore $F$ is $[l_{0},\ldots,l_{m}]$-partitioned, $P\ F$ holds, $\bigcup F\subseteq\{\overline{n}\}$, $|A|=m$ and $A\subseteq\{\overline{n}\}$. Since $\overline{P}$ incrementally checks $P$, since for all $A^{\prime}\in F$, it holds that $|A|=m\geq|A|^{\prime}$, since $A\notin F$, and since $P\ F$ and $\overline{P}\ F\ A$ hold, by relation (1), $P\ (F\cup\{A\})$ must hold. Moreover, since $A\notin F$, since $F$ is $[l_{0},\ldots,l_{m}]$-partitioned, and since $|A|=m$, it holds that $F\cup\{A\}$ is $[l_{0},\ldots,l_{m}+1]$-partitioned. Finally, $\bigcup F^{\prime}=\bigcup F\cup A\subseteq\{\overline{n}\}$. Therefore, $F^{\prime}=F\cup\{A\}\in{[l_{0},\ldots,l_{m}+1]}_{n}^{P}$.

A.4 Proof of Theorem 4

Theorem 4

Assume that the predicate $\overline{P}$ incrementally checks $P$ and is preserved by injective functions. If $m\leq n$ and $\mathcal{F}_{b}$ is an iso-representing subcollection of ${[l_{0},\ldots,l_{m}]}_{n}^{P}$, then $\mathcal{F}^{\prime}_{b}\equiv\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m}$ is an iso-representing subcollection of ${[l_{0},\ldots,l_{m}+1]}_{n}^{P}$.

Proof 6

$\mathcal{F}^{\prime}_{b}$* is a subcollection of ${[l_{0},\ldots,l_{m}+1]}_{n}^{P}$. Indeed, since $\mathcal{F}_{b}$ is a subcollection of ${[l_{0},\ldots,l_{m}]}_{n}^{P}$, and $\mathcal{F}^{\prime}_{b}\equiv\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m}$, the statement holds by Theorem 3.*

Let us show that $\mathcal{F}^{\prime}_{b}$ iso-represents ${[l_{0},\ldots,l_{m}+1]}_{n}^{P}$. Let $F^{\prime}$ be an arbitrary element of ${[l_{0},\ldots,l_{m}+1]}_{n}^{P}$. By Theorem 3, there is a family $F\in{[l_{0},\ldots,l_{m}]}_{n}^{P}$ and a set $A\in\binom{\{\overline{n}\}}{m}$ such that $F^{\prime}=F\cup{A}$, $A\notin F$, $\overline{P}\ A\ F$. Since $\mathcal{F}_{b}$ iso-represents ${[l_{0},\ldots,l_{m}]}_{n}^{P}$, there is a family $F_{b}\in\mathcal{F}_{b}$ such that $F\cong F_{b}$, i.e., there is a bijection $f$ between $\bigcup F$ and $\bigcup F_{b}$ such that $F_{b}=f`F$.

There is a function $f^{\prime}$, extending $f$ from $\bigcup F$ to $\bigcup F\cup A$, such that it is injective on $\bigcup F\cup A$, that $f^{\prime}`F=F_{b}$ and that $f^{\prime}`(F\cup\{A\})\subseteq\{\overline{n}\}$.

Let $A_{b}$ denote the set $f^{\prime}`A$. The function $f^{\prime}$ establishes an isomorphism between $F\cup\{A\}$ and $f^{\prime}`F\cup\{f^{\prime}`A\}$, i.e., $F_{b}\cup\{A_{b}\}$. Therefore $F^{\prime}\cong F_{b}\cup\{A_{b}\}$. Moreover, $F_{b}\cup\{A_{b}\}$ is in $\mathcal{F}^{\prime}_{b}$. Indeed, it holds that $F_{b}\in\mathcal{F}_{b}$. Also, since $f^{\prime}$ is an injection from $\bigcup F\cup A$ into $\{\overline{n}\}$, it holds that $|A_{b}|=|A|=m$, and $A_{b}\subseteq\{\overline{n}\}$, and, since $A\notin F$ it holds that $f^{\prime}`A\notin f^{\prime}`F$ i.e., $A_{b}\notin F_{b}$. Finally, since $\overline{P}$ is preserved by injective functions it also holds that $\overline{P}\ (f^{\prime}`F)\ (f^{\prime}`A)$, i.e., $\overline{P}\ F_{b}\ A_{b}$. Therefore, $\mathcal{F}^{\prime}_{b}$ iso-represents ${[l_{0},\ldots,l_{m}+1]}_{n}^{P}$.

A.5 Proof of Theorem 5

The characterization of this procedure (in terms of relation that connects the list given as its parameter and the returned value for corresponding to that list) is given by the following proposition. This proposition is proved using mathematical induction, based on the definition of ${\sf enum\_rec}$.

Proposition 24

Let $L$ be a given list, and $R$ be a relation between a value and a list. If

$R\ v_{[\,]}\ [\,]$, 2. 2.

for all $v^{\prime}$ and $L^{\prime}$, if $R\ v^{\prime}\ L^{\prime}$, then $R\ v^{\prime}\ [L^{\prime},0]$, 3. 3.

for all $v^{\prime}$ and $L^{\prime}$, if $L^{\prime}$ is not empty, ${\sf last}\ L^{\prime}>0$, $|L^{\prime}|\leq|L|$, and

$R\ v^{\prime}\ ({\sf dec\_last}\ L^{\prime})$, then $R\ (upd\ v^{\prime}\ L^{\prime})\ L^{\prime}$,

then $R\ ({\sf enum\_rec}^{v_{[\,]}\,upd}\ L)\ L$.

Finally, we show how can we use ${\sf enum\_rec}$ to find an iso-base of ${{L}}_{n}^{P}$ for some given list $L$, number $n$, and a predicate $P$.

Theorem 5

Let $L$ be a list such that $|L|\leq n+1$. Assume that:

$P\ \{\}$* holds and $v_{[\,]}=\{\{\}\}$,* 2. 2.

$\overline{P}$* incrementally checks $P$ and is preserved by injective functions,* 3. 3.

$\mathcal{P}$* contains all permutations of $[\overline{n}]$, and $upd=\lambda\ \mathcal{F}\ L.\ iso\_reduce_{\mathcal{P}}\ (\mathcal{F}\odot_{\overline{P}}\binom{\{\overline{n}\}}{|L|-1})$.*

Then ${\sf enum\_rec}^{v_{[\,]}\,upd}\ L$ is an iso-base of ${{L}}_{n}^{P}$.

Proof 7

The result follows by Proposition 24 ($R\ v\ L$ holds iff $v$ is an iso-base of ${L}_{n}^{P}$). All the conditions of Proposition 24 are met.

Since $P\ \{\}$ holds, ${[\,]}_{n}^{P}=\{\{\}\}$, so $v_{[\,]}=\{\{\}\}$ is its iso-base. 2. 2.

It holds that ${L}_{n}^{P}={[L,0]}_{n}^{p}$. So, if some $\mathcal{F}_{b}$ is an iso-base of ${L}_{n}^{P}$, then it is also an iso-base of ${[L,0]}_{n}^{p}$. 3. 3.

Let $L^{\prime}$ be a nonempty list, such that ${\sf last}\ L^{\prime}>0$, and $|L^{\prime}|\leq|L|$. Then, for some $m\geq 0$, $L^{\prime}=[l_{0},\ldots,l_{m}]$, $l_{m}>0$, ${\sf dec\_last}\ L^{\prime}=[l_{0},\ldots,l_{m}-1]$, and $|L^{\prime}|-1=m$. Let $v^{\prime}\equiv\mathcal{F}_{b}$ be an iso-base of ${\sf dec\_last}\ L^{\prime}$. By the definition of $upd$, it holds that $upd\ \mathcal{F}_{b}\ L^{\prime}=iso\_reduce_{\mathcal{P}}\ (\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m})$. Since $m\leq n$, by Theorem 4, $\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m}$ is an iso-representing set of ${L^{\prime}}_{n}^{P}$. Therefore, since $\mathcal{P}$ contains all permutations of $[\overline{n}]$ and $\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m}\subseteq\{\!\{\overline{n}\}\!\}$, $iso\_reduce_{\mathcal{P}}\ (\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m})$ is an iso-base of ${L^{\prime}}_{n}^{P}$.

A.6 Proof of Theorem 6

The procedure ${\sf enum\_dp\_aux}^{L_{max}\,stop\,upd}\ L\ v\ m\ res$ is characterized by the following proposition.

Proposition 25

Let $R$ be a relation between a value and a list. Let $L_{max}$ be a fixed list, and $stop$ a predicate for lists. Let $L\equiv[l_{0},\ldots,l_{m},0,\ldots,0]$ be a given (initial) list (i.e., $m<|L|$, $\forall k.\ m<k<|L|\ \longrightarrow\ l_{k}=0$) such that $|L|=|L_{max}|$. Let $v$ be a value. Assume that:

$R\ v\ L$, 2. 2.

for all $v^{\prime}$, $L^{\prime}$ and $m^{\prime}$, such that $m^{\prime}<|L|$ and $L^{\prime}\equiv[l^{\prime}_{0},\ldots,l^{\prime}_{m^{\prime}},0,\ldots,0]$ (i.e., $m^{\prime}<|L^{\prime}|$, and $\forall k.\ m^{\prime}<k<|L|\ \longrightarrow\ l^{\prime}_{k}=0$) it holds that if $R\ v^{\prime}\ L^{\prime}$, then $R\ (upd\ v^{\prime}\ m^{\prime})\ ({\sf inc\_nth}\ L^{\prime}\ m^{\prime})$.

Then, for all $L^{\prime}$ such that $L\preceq L^{\prime}\preceq L_{max}$, such that $L$ and $L^{\prime}$ agree up to the position $m$ (i.e., $L^{\prime[m]}=L^{[m]}$), and such that there is no $L_{s}$ such that $L\preceq L_{s}\preceq L^{\prime}$, $L_{s}^{[m]}=L^{[m]}$ and $stop\ L_{s}$, there is a $v^{\prime}\in({\sf enum\_dp\_aux}^{L_{max}\,stop\,upd}\ L\ v\ m\ res)$ such that $R\ v^{\prime}\ L^{\prime}$

The proof of Theorem 6 relies on this Proposition.

Theorem 6

Assume that

$\overline{P}$* incrementally checks $P$ and is preserved by injective functions,* 2. 2.

$P\ \{\}$* holds and $v_{[\,]}=\{\{\}\}$,* 3. 3.

$L_{max}$* is a list such that $|L_{max}|\leq n+1$, $\mathcal{L}_{s}$ contain lists (that all have the same length $|L_{max}|$), and $stop=\lambda\ L.\ (\exists L_{s}\in\mathcal{L}_{s}.\ L\succeq L_{s})$,* 4. 4.

$\mathcal{P}$* contains all permutations of $[\overline{n}]$, $upd=\lambda\ \mathcal{F}\ m.\ iso\_reduce_{\mathcal{P}}\ (\mathcal{F}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m})$.*

Let $X=\{L.\ L\preceq L_{max}\wedge(\nexists L_{s}\in\mathcal{L}_{s}.\ L\succeq L_{s})\}$. Then, for all $L\in X$, there exists an $\mathcal{F}_{b}\in{\sf enum\_dp}\ {L_{max}\ stop\ upd\ v_{[\,]}}$ such that $\mathcal{F}_{b}$ is an iso-base of ${L}_{n}^{P}$.

Proof 8

The proof relies on Proposition 25 ($R\ v\ L$ holds iff $v$ is an iso-base of ${L}_{n}^{P}$). The function ${\sf enum\_dp\_aux}$ is called for list $L=[0,\ldots,0]$ so the initial assumptions are trivially satisfied.

Next we need to show that $v_{[\,]}=\{\{\}\}$ is an iso-base of ${[0,\ldots,0]}_{n}^{P}$. But, it holds that ${[0,\ldots,0]}_{n}^{P}={[\,]}_{n}^{P}$, and since $P\{\}$ holds, ${[\,]}_{n}^{P}=\{\{\}\}$ so $\{\{\}\}$ is its iso-base.

Let us show the final assumption. Fix a collection $v^{\prime}\equiv\mathcal{F}_{b}$, list $L^{\prime}$ and $m^{\prime}<|L^{\prime}|$, $m^{\prime}<|L|$ such that $L^{\prime}$ is of the form $[l^{\prime}_{0},\ldots,l^{\prime}_{m^{\prime}},0,\ldots,0]$ and assume that $\mathcal{F}_{b}$ is an iso-base of ${L^{\prime}}_{n}^{P}$. Then $\mathcal{F}_{b}$ is also an iso-base of ${[l^{\prime}_{0},\ldots,l^{\prime}_{m^{\prime}}]}_{n}^{P}$. It holds that $upd\ \mathcal{F}_{b}\ m^{\prime}=iso\_reduce_{\mathcal{P}}\ (\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m^{\prime}})$. Since $\overline{P}$ incrementally checks $P$ and is preserved by injective functions, and since $m^{\prime}<|L|=|L_{max}|\leq n+1$, by Theorem 4, $\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m^{\prime}}$ is an iso-representing set of ${[l^{\prime}_{0},\ldots,l^{\prime}_{m^{\prime}}+1]}_{n}^{P}$. Therefore, since $\mathcal{P}$ contains all permutations of $[\overline{n}]$ and $\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m^{\prime}}\subseteq\{\!\{\overline{n}\}\!\}$, the collection $iso\_reduce_{\mathcal{P}}\ (\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m})$ is an iso-base of ${[l^{\prime}_{0},\ldots,l^{\prime}_{m^{\prime}}+1]}_{n}^{P}$. But, since, $inc\_nth\ L^{\prime}\ m^{\prime}=[l^{\prime}_{0},\ldots,l^{\prime}_{m^{\prime}}+1,0,\ldots,0]$, that is equal to $[l^{\prime}_{0},\ldots,l^{\prime}_{m^{\prime}}+1]$, it holds that $iso\_reduce_{\mathcal{P}}\ (\mathcal{F}_{b}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m^{\prime}})$ is also an iso-base of ${(inc\_nth\ L^{\prime}\ m^{\prime})}_{n}^{P}$.

Since ${\sf enum\_dp}$ calls ${\sf enum\_dp\_aux}$ for $L=[0,\ldots,0]$ and $m=0$, and since $\succeq$ is transitive, the set of all $L^{\prime}$ such that $L\preceq L^{\prime}\preceq L_{max}$, $L^{\prime[m]}=L^{[m]}$ and such that there is no $L_{s}$ such that $L\preceq L_{s}\preceq L^{\prime}$, $L_{s}^{[m]}=L^{[m]}$ and $stop\ L_{s}$ is exactly the set $X$. Therefore, the statement holds.

A.7 Proof of Lemma 1

Lemma 1

If $F$ and $F^{\prime}$ are both irreducible families and $\left\langle F\right\rangle=\left\langle F^{\prime}\right\rangle$, then $F=F^{\prime}$.

Proof 9

Let us first show that if $F^{\prime}$ is an irreducible family and $\left\langle F\right\rangle=\left\langle F^{\prime}\right\rangle$, then $F^{\prime}\subseteq F$.

Assume the opposite. Then there is a set $A$ such that $A\in F^{\prime}$ and $A\notin F$. Since $A\in F^{\prime}\subseteq\left\langle F^{\prime}\right\rangle=\left\langle F\right\rangle$, there is a nonempty family $F_{A}\subseteq F$ such that $\bigcup F_{A}=A$. The family $F_{A}$ can be split to $F_{A}^{+}=F_{A}\cap F^{\prime}$ and $F_{A}^{-}=F_{A}\setminus F^{\prime}$. All elements in $F_{A}^{-}$ belong to $F_{A}\subseteq F\subseteq\left\langle F\right\rangle=\left\langle F^{\prime}\right\rangle$, so for every $A^{\prime}\in F_{A}^{-}$ there is a non-empty family $F^{A^{\prime}}\subseteq F^{\prime}$ such that $A^{\prime}=\bigcup{F^{A^{\prime}}}$. Let $G$ be a family consisting of $F_{A}^{+}$ and union of all such families $F^{A^{\prime}}$ for each element $A^{\prime}\in F_{A}^{-}$.

The family $G$ is a subfamily of $F^{\prime}$. Indeed, $F_{A}^{+}=F_{A}\cap F^{\prime}\subseteq F^{\prime}$ and for all $F^{A^{\prime}}$ it holds that $F^{A^{\prime}}\subseteq F^{\prime}$.

It holds that $\bigcup{G}=A$. Namely, it holds that the union of all families $F^{A^{\prime}}$ over all elements $A^{\prime}\in F_{A}^{-}$ is equal to the $\bigcup F_{A}^{-}$. Therefore, $\bigcup{G}=\bigcup{F_{A}^{+}}\cup\bigcup{F_{A}^{-}}=\bigcup{F_{A}}=A$.

The set $A$ is not in $G$. Assume the opposite. Then, since $A\notin F$ and $F_{A}\subseteq F$, it holds that $A\notin F_{A}^{+}\subseteq F_{A}$. Therefore, $A$ must belong to some family $F^{A^{\prime}}$ for some $A^{\prime}\in F_{A}^{-}$. Hence, $A^{\prime}\in F_{A}$ so $A^{\prime}\subseteq\bigcup{F_{A}}=A$. Also, since $\bigcup{F^{A^{\prime}}}=A^{\prime}$ and $A\in F^{A^{\prime}}$ it must be that $A\subseteq A^{\prime}$. So $A=A^{\prime}$ and $A\in F_{A}\subseteq F$ which contradicts that $A\notin F$.

The family $G$ is not empty. Indeed, since $F_{A}$ is not empty it contains a set $A^{\prime}$. If $A^{\prime}\in F^{\prime}$, then $A^{\prime}\in F_{A}\cap F^{\prime}=F_{A}^{+}\subseteq G$ so $G$ is not empty. If $A^{\prime}\notin F^{\prime}$, then $A^{\prime}\in F_{A}\setminus F^{\prime}=F_{A}^{-}$. But, then there is a non-empty family $F^{A^{\prime}}$ whose elements are in $G$, so $G$ is not empty.

From all this, it follows that $A$ depends on elements of $F^{\prime}\setminus\{A\}$. But, since $A\in F^{\prime}$, this contradicts that $F^{\prime}$ is irreducible, so the initial assumption was wrong and $F^{\prime}\subseteq F$.

The main statement is a trivial consequence of the one that we have just proved.

A.8 Proof of Lemma 2

Lemma 2

Any family $F$ that is FC-covered by an FC-family $F_{c}$ is an FC-family. 2. 2.

Any family $F$ that is nonFC-covered by a nonFC-family $N_{c}$ is not an FC-family.

Proof 10

Since $F_{c}\vdash F$, there is a family $F_{c}^{\prime}$ such that $F_{c}\cong F_{c}^{\prime}$ and $\left\langle F\right\rangle\supseteq F_{c}^{\prime}$. Since $F_{c}$ is an FC-family, so is $F_{c}^{\prime}$. Therefore, by Proposition 2, $\left\langle F\right\rangle$ is an FC-family. But, then, by Proposition 4, $F$ is also an $FC$ family. 2. 2.

Since $N_{c}\Vdash F$, there is a family $N_{c}^{\prime}$ such that $\left\langle F\right\rangle\subseteq\left\langle N_{c}^{\prime}\right\rangle\cup\{\{\}\}$. If $F$ were an FC-family, since $F\subseteq\left\langle F\right\rangle\subseteq\left\langle N_{c}^{\prime}\right\rangle\cup\{\{\}\}$, by Proposition 2 and Proposition 3, $N_{c}^{\prime}$ would also be FC-family, which is a contradiction, as it isomorphic to a nonFC-family $N_{c}$.

A.9 Proof of Lemma 3

Lemma 3

Assume that $\mathcal{F}_{b}$ iso-represents $\mathcal{F}$. If $\mathcal{F}_{c}\vdash\mathcal{F}_{b}$, then $\mathcal{F}_{c}\vdash\mathcal{F}$. If $\mathcal{N}_{c}\Vdash\mathcal{F}_{b}$, then $\mathcal{N}_{c}\Vdash\mathcal{F}$. If $(\mathcal{F}_{c},\mathcal{N}_{c})\vDash\mathcal{F}_{b}$, then $(\mathcal{F}_{c},\mathcal{N}_{c})\vDash\mathcal{F}$.

Proof 11

Let $F\in X$. Since $\mathcal{F}_{b}$ iso-represents $X$, there is an $F^{\prime}\in\mathcal{F}_{b}$ such that $F\cong F^{\prime}$. If $\mathcal{F}_{c}\vdash\mathcal{F}_{b}$, then $\mathcal{F}_{c}\vdash F^{\prime}$. But then, by Proposition 15, $\mathcal{F}_{c}\vdash F$. Similarly, if $\mathcal{N}_{c}\Vdash\mathcal{F}_{b}$, then $\mathcal{N}_{c}\Vdash F^{\prime}$. But then, by Proposition 15, $\mathcal{N}_{c}\Vdash F$. If $(\mathcal{F}_{c},\mathcal{N}_{c})\vDash\mathcal{F}_{b}$, then either $\mathcal{F}_{c}\vdash F^{\prime}$ or $\mathcal{N}_{c}\Vdash F^{\prime}$. But then, by Proposition 15 either $\mathcal{F}_{c}\vdash F$ or $\mathcal{N}_{c}\Vdash F$, so $(\mathcal{F}_{c},\mathcal{N}_{c})\vDash F$.

A.10 Proof of Lemma 4

Lemma 4

If all irreducible families in $\{\!\{\overline{n}\}\!\}$ are covered by $\mathcal{F}_{c}$ and $\mathcal{N}_{c}$, then all families in $\{\!\{\overline{n}\}\!\}$ are covered by $\mathcal{F}_{c}$ and $\mathcal{N}_{c}$.

Proof 12

Fix an arbitrary family $F\in\{\!\{\overline{n}\}\!\}$. By Proposition 14, there is an irreducible family $F^{\prime}$ such that $F^{\prime}\subseteq F$ and $\left\langle F\right\rangle=\left\langle F^{\prime}\right\rangle$. Since $F^{\prime}\in\{\!\{\overline{n}\}\!\}$, by assumption it is covered by $\mathcal{F}_{c}$ and $\mathcal{N}_{c}$. But then, by Proposition 16, so is $F$.

A.11 Proof of Lemma 5

Lemma 5

For every list $L\in\mathcal{L}_{F}$ all $L$-partitioned families of $\{\!\{\overline{6}\}\!\}$ are FC-covered by $\mathcal{F}_{c}^{6}$. For every list $L\in\mathcal{L}_{N}$, all $L$-partitioned families of $\{\!\{\overline{6}\}\!\}$ are nonFC-covered by $\mathcal{N}_{c}^{6}$.

Proof 13

Let $P=\lambda F.\ \neg(\mathcal{F}_{c}^{6}\vdash F)$ and $\overline{P}=\lambda\ F\ A.\ \neg(\mathcal{F}_{c}^{6}\vdash F\cup\{A\})$. Let $v_{[\,]}=\{\{\}\}$. Let $\mathcal{P}_{6}$ contain all permutations of $[\overline{6}]$ and $upd=\lambda\ \mathcal{F}\ L.\ iso\_reduce_{\mathcal{P}_{6}}\ (\mathcal{F}\odot_{\overline{P}}\binom{\{\overline{6}\}}{|L|-1})$. All conditions of Lemma 5 are met, so it holds that ${\sf enum\_rec}^{v_{[\,]}\,upd}\ L$ is an iso-base of ${{L}}_{6}^{P}$. Evaluating it for all $L\in\mathcal{L}_{F}$ gives $\{\}$. Therefore, for any $L\in\mathcal{L}_{F}$ there are no families in $\{\!\{\overline{6}\}\!\}$ that are $L$-partitioned an are not FC-covered by $\mathcal{F}_{c}^{6}$.

Let $P$ and $\overline{P}$ be $\top$. Let $v_{[\,]}=\{\{\}\}$. Let $\mathcal{P}_{6}$ contain all permutations of $[\overline{6}]$ and $upd=\lambda\ \mathcal{F}\ L.\ iso\_reduce_{\mathcal{P}_{6}}\ (\mathcal{F}\odot_{\overline{P}}\binom{\{\overline{6}\}}{|L|-1})$. By Lemma 5, ${\sf enum\_rec}^{v_{[\,]}\,upd}\ L$ is an iso-base of all $L$-partitioned families of $\{\!\{\overline{6}\}\!\}$. After evaluating it for any $L\in\mathcal{L}_{N}$, a direct computation shows that all its members are nonFC-covered by $\mathcal{N}_{c}^{6}$.

A.12 Proof of Lemma 6

Lemma 6

If for all $L\in\mathfrak{L}_{F}$, there exists a collection $\mathcal{F}^{L}_{b}$ that iso-represents ${L}_{6}^{ir}$ such that $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash\mathcal{F}^{L}_{b}$, then $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash\{\!\{\overline{6}\}\!\}$.

Proof 14

First we prove that for all $L\in\mathfrak{L}_{F}$, it holds that $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash{L}_{6}^{ir}$. Let $L$ be an arbitrary list in $\mathfrak{L}_{F}$. By assumption there exists $\mathcal{F}^{L}_{b}$ that iso-represents ${L}_{6}^{ir}$, such that $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash\mathcal{F}^{L}_{b}$. Then, by Lemma 3, it holds that $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash{L}_{6}^{ir}$.

To show that for all $F\in\{\!\{\overline{6}\}\!\}$ it holds that $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash F$, by Lemma 4 it suffices to show that all irreducible families in $\{\!\{\overline{6}\}\!\}$ are covered by $\mathcal{F}_{c}^{6}$ and $\mathcal{N}_{c}^{6}$.

Fix an arbitrary irreducible family $F$ in $\mathcal{F}_{b}$. By Proposition 18, $F$ is $L$-partitioned for some $L=[l_{0},\ldots,l_{6}]$ and $L\preceq[1,6,15,20,15,6,1]$.

If there is a list $L^{\prime}\in\mathcal{L}_{F}$ such that $L\succeq L^{\prime}$, then, by Lemma 5 for all $F^{\prime}$ in $\{\!\{\overline{6}\}\!\}$ that are $L^{\prime}$-partitioned it holds that $\mathcal{F}_{c}^{6}\vdash F^{\prime}$, so by Proposition 19 it holds that $\mathcal{F}_{c}^{6}\vdash F$ (as $F$ is $L$-partitioned and $L\succeq L^{\prime}$) and therefore $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash F$.

Otherwise, $L\in\mathfrak{L}_{F}$, and by our first proved statement it holds that $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash{L}_{6}^{ir}$. It holds that $l_{0}=0$ or $l_{0}=1$.

If $l_{0}=0$, then $F$ is irreducible, $L$-partitioned family, where $L\in\mathfrak{L}_{F}$, i.e., $F\in{L}_{6}^{ir}$, so, since $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash{L}_{6}^{ir}$, it holds that $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash F$.

If $l_{0}=1$, then $F-\{\{\}\}$ is irreducible, $[0,l_{1},\ldots,l_{6}]$-partitioned family, where $[0,l_{1},\ldots,l_{6}]\in\mathfrak{L}_{F}$, i.e., $F-\{\{\}\}\in{L}_{6}^{ir}$, so, since $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash{L}_{6}^{ir}$, it holds that $F-\{\{\}\}$ is covered by $\mathcal{F}_{c}^{6}$ and $\mathcal{N}_{c}^{6}$. But then, by Proposition 15, so is $F$.

A.13 Proof of Theorem 8

Theorem 8

It holds that $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash\{\!\{\overline{6}\}\!\}$.

Proof 15

Let $P=\lambda F.\ \mathit{ir}\ F\ \wedge\ \neg(\mathcal{F}_{c}^{6}\vdash F)$ and $\overline{P}=\lambda\ F\ A.\ \neg\ \mathit{depends}\ A\ F\wedge\ \neg(\mathcal{F}_{c}^{6}\vdash F\cup\{A\})$. It holds that $\overline{P}$ incrementally checks $P$ and is preserved by injective functions. Let $val_{[\,]}=\{\{\}\}$, $L_{max}=[0,6,15,20,15,6,1]$, and $stop=\lambda\ L.\ (\exists L_{s}\in\mathcal{L}_{F}.\ L\succeq L_{s})$. Let $\mathcal{P}$ contain all permutations of $[\overline{6}]$, and $upd=\lambda\ \mathcal{F}\ m.\ iso\_reduce_{\mathcal{P}}\ (\mathcal{F}\odot_{\overline{P}}\binom{\{\overline{n}\}}{m})$.

By Theorem 6, for all lists $L=[0,\ldots,l_{6}]\in\mathfrak{L}_{F}$, there exists a collection $\mathcal{F}^{L}_{b}\in{\sf enum\_dp}\ {L_{max}\ stop\ upd\ v_{[\,]}}$ such that $\mathcal{F}^{L}_{b}$ is an iso-base of ${L}_{6}^{P}$. By definition of $P$, $\mathcal{F}^{L}_{b}$ is an iso-base of all members of ${L}_{6}^{ir}$ that are not covered by $\mathcal{F}_{c}^{6}$. However, a direct computation shows that all families in ${\sf enum\_dp}\ {L_{max}\ stop\ upd\ v_{[\,]}}$ are covered by $\mathcal{N}_{c}^{6}$. Therefore all members of $\mathcal{F}^{L}_{b}$ are covered by $\mathcal{N}_{c}^{6}$, so by Lemma 3, all elements of ${L}_{6}^{ir}$ that are not covered by $\mathcal{F}_{c}^{6}$ are covered by $\mathcal{N}_{c}^{6}$. In other words, for all $F\in{L}_{6}^{ir}$ it holds that $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash F$, i.e., $(\mathcal{F}_{c}^{6},\mathcal{N}_{c}^{6})\vDash{L}_{6}^{ir}$. As ${L}_{6}^{ir}$ iso-represents itself, by Lemma 6, all sets in $\{\!\{\overline{6}\}\!\}$ are covered.

Appendix B Statistics

As a byproduct of our classification, we have counted the number of FC and nonFC families. For each each list $L=[l_{0},\ldots,l_{6}]$ we have counted $L$-partititioned families and calculated: (a) the total number of non-isomorphic FC-families and the total number of non-isomorphic nonFC-families, (b) the total number of non-isomorphic irreducible FC-families and the total number of non-isomorphic nonFC-families, (c) the total number of minimal FC-families and the total number of maximal nonFC-families. This data is summarized in a spreadsheat available online (http://argo.matf.bg.ac.rs/downloads/formalizations/FCFamilies.xls).